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