多重集合重写与Spi演算的安全协议分析方法

当形式化描述安全协议时,不同的规范语言采用不同的推理方法,其结果不能直接或容易地进行比较,因此在不同的框架中建立明确的关联是必要的。论文在多重集合重写MSR和Spi演算的形式化规范之间建立关联,并定义了一种双射;提出和证明了MSR和Spi演算之间在分析安全协议安全性时的一致性关系定理,利用这个关系对Needham-Schroeder公钥协议进行安全性分析。