通信学报 ›› 2012, Vol. 33 ›› Issue (Z1): 250-254.doi: 10.3969/j.issn.1000-436x.2012.z1.033

• 学术论文 • 上一篇    下一篇

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

鲁来凤1,段新东2,马建峰3   

  1. 1 陕西师范大学 数学与信息科学学院,陕西 西安 710062
    2 南阳理工学院 软件学院,河南 南阳 473004
    3 西安电子科技大学 计算机网络与信息安全教育部重点实验室,陕西 西安 710071
  • 出版日期:2012-09-25 发布日期:2017-08-03
  • 基金资助:
    国家自然科学基金资助项目;陕西省自然科学基金资助项目;陕西省自然科学基金资助项目;中央高校基本科研业务费基金资助项目;中央高校基本科研业务费基金资助项目;中央高校基本科研业务费基金资助项目

Improvement and formal proof on protocol Otway-Rees

Lai-feng LU1,Xin-dong DUAN2,Jian-feng MA3   

  1. 1 College of Mathematics and Information Science,Shaanxi Normal University,Xi’an 710062,China
    2 School of Software Nan Yang Institute of Technology,Nanyang 430074,China
    3 Ministry of Education Key Laboratory of Computer Networks and Information Security,Xidian University,Xi’an 710071,China
  • Online:2012-09-25 Published:2017-08-03
  • Supported by:
    The National Natural Science Foundation of China;The Natural Science Foundation of Shaanxi Province;The Natural Science Foundation of Shaanxi Province;The Fundamental Research Funds for the Central Universities;The Fundamental Research Funds for the Central Universities;The Fundamental Research Funds for the Central Universities

摘要:

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

关键词: 安全协议, 形式化方法, 协议组合逻辑, Otway-Rees协议

Abstract:

Choosing the authentication key distribution protocol Otway-Rees as the research object,using protocol composition logic (PCL) as proof tool,the security protocol analysis and formal proof was studied.Firstly,this paper gave the forms of security attack,analyzed the Otway-Rees defects and put forward the amended protocol (named as AOR protocol).Then,PCL was extended.And then PCL was used to describe and prove the behavior of each entity and the safety of the protocol attribute formally.Finally,the conclusion was given that the amended AOR protocol has the security attribute of key confidentiality.

Key words: security protocol, formal methods, protocol composition logic, protocol Otway-Rees

No Suggested Reading articles found!