基于进程代数的Otway-Rees协议的形式化验证  

Formal Verification of Otway-Rees Protocol Based on Process Algebra

作　　者：蔡雨桐 王勇 王然然 姜正涛[2] 代桂平 CAI Yu-tong;WANG Yong;WANG Ran-ran;JIANG Zheng-tao;DAI Gui-ping(College of Computer Science and Technology,Faculty of Information Technology,Beijing University of Technology,Beijing 100124,China;School of Computer Science and Cybersecurity,Communication University of China,Beijing 100024,China;College of Artificial Intelligence and Automation,Faculty of Information Technology,Beijing University of Technology,Beijing 100124,China)

机构地区：[1]北京工业大学信息学部计算机学院,北京100124 [2]中国传媒大学计算机与网络空间安全学院,北京100024 [3]北京工业大学信息学部人工智能与自动化学院,北京100124

出　　处：《计算机科学》2021年第S01期477-480,共4页Computer Science

基　　金：广西密码学与信息安全重点实验室研究课题(GCIS201808)。

摘　　要：Otway-Rees协议的目的是完成发起者和响应者之间的双向认证,并且分发服务器产生的会话密钥。该协议的特点是简单实用,没有使用复杂的同步时钟机制或双重加密,仅用少量的信息提供了良好的时效性。此协议允许通过一个网络的个别通信认证自己的身份,还可以阻止重放攻击和窃听,允许修改检测。对安全协议的分析是信息时代无法回避的关键问题,事实证明,形式化方法是安全协议分析更为可靠和有效的途径。此协议的形式化验证对于工程实施具有重要意义。对Otway-Rees协议进行抽象处理,得到抽象模型,在此基础上给出基于进程代数的形式化描述,并进行形式化验证。验证结果表明,此协议形式的并行系统展现出了期望的外部行为。Otway-Rees protocol is to complete the two-way authentication between the initiator and the responder, and to distri-bute the session key generated by the server.The feature of this protocol is simple and practical.It does not use complicated synchronous clock mechanism or double encryption, and provides good timeliness with only a small amount of information.This protocol allows individual communications to be authenticated through a network, while also preventing replay attacks and eavesdropping, as well as modifying detection.The analysis of security protocols is a key issue that cannot be avoided in the information age.Formal method, which is based on strict mathematical and mechanical methods, is an important method to improve and ensure the quality of computing system.Its model, technology and tools have become an important carrier of computing thinking.The formal method can accurately reveal all kinds of logic rules, make corresponding logic rules, and make all kinds of theoretical systems more rigorous.Formal method is a mathematical description of what a program does, a description of the function of a program written in a formal language with precise semantics.It is not only the starting point of designing and programming, but also the basis of verifying whether a program is correct, so as to improve the reliability and robustness of the design.By abstracting the Otway-Rees protocol, we can get the abstract model.On this basis, the formal description based on process algebra is gi-ven and the formal verification is carried out.The verification results show that the parallel system in the form of this protocol shows the expected external behavior.

关 键 词：Otway-Rees 安全协议 协议验证 形式化 进程代数 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]