论文部分内容阅读
安全协议模型是安全协议分析与验证的基础,现有的建模方法中存在着一些缺点,如:建模复杂、重用性差等.为此提出了一种类型化的π演算:π^t演算,并给出了相应类型推理规则和求值规则,π^t演算的安全性也得到了证明.π^t演算可以对安全协议、协议攻击者进行形式化建模.基于π^t演算的安全协议模型及其建模过程使用NRL协议为例做出了说明.同时给出了攻击者模型,并证明了基于π^t演算的安全协议攻击者模型与D—Y攻击者模型在行动能力上是一致的.这保证了基于π^t演算的安全协议模型的验证结果的正确性.基于π^t演算的建模