Otway-Rees协议改进及形式化证明  

Improvement and formal proof on protocol Otway-Rees

作　　者：鲁来凤[1] 段新东[2] 马建峰[3] 

机构地区：[1]陕西师范大学数学与信息科学学院,陕西西安710062 [2]南阳理工学院软件学院,河南南阳473004 [3]西安电子科技大学计算机网络与信息安全教育部重点实验室,陕西西安710071

出　　处：《通信学报》2012年第S1期250-254,共5页Journal on Communications

基　　金：国家自然科学基金资助项目(61173190);陕西省自然科学基金资助项目(2009JM8002;2012JQ8023);中央高校基本科研业务费基金资助项目(GK200902051;GK201002041;GK201002037)~~

摘　　要：选取认证密钥分配协议Otway-Rees协议作为研究对象,利用协议组合逻辑(PCL)作为协议证明工具,对安全协议形式化分析及证明进行了研究。首先给出了Otway-Rees协议常见的攻击形式,分析了存在的缺陷,提出了改进方案(AOR协议);然后,为了更好地形式化描述AOR协议,对传统的PCL进行一定的扩展;紧接着,用扩展后的PCL对改进的协议中各个实体的行为和协议的安全属性进行形式化描述,将改进后的协议进行模块化划分,并利用PCL进行组合证明;最后,得出改进后的AOR协议具有密钥保密属性。选取认证密钥分配协议Otway-Rees协议作为研究对象,利用协议组合逻辑(PCL)作为协议证明工具,对安全协议形式化分析及证明进行了研究。首先给出了Otway-Rees协议常见的攻击形式,分析了存在的缺陷,提出了改进方案(AOR协议);然后,为了更好地形式化描述AOR协议,对传统的PCL进行一定的扩展;紧接着,用扩展后的PCL对改进的协议中各个实体的行为和协议的安全属性进行形式化描述,将改进后的协议进行模块化划分,并利用PCL进行组合证明;最后,得出改进后的AOR协议具有密钥保密属性。

关 键 词：安全协议 形式化方法 协议组合逻辑 OTWAY-REES协议 

分 类 号：TN91-55[电子电信—通信与信息系统]