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

摘要：

Otway-Rees协议的目的是完成发起者和响应者之间的双向认证,并且分发服务器产生的会话密钥.该协议的特点是简单实用,没有使用复杂的同步时钟机制或双重加密,仅用少量的信息提供了良好的时效性.此协议允许通过一个网络的个别通信认证自己的身份,还可以阻止重放攻击和窃听,允许修改检测.对安全协议的分析是信息时代无法回避的关键问题,事实证明,形式化方法是安全协议分析更为可靠和有效的途径.此协议的形式化验证对于工程实施具有重要意义.对Otway-Rees协议进行抽象处理,得到抽象模型,在此基础上给出基于进程代数的形式化描述,并进行形式化验证.验证结果表明,此协议形式的并行系统展现出了期望的外部行为.

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

所属期刊栏目：48

分类号：TP301.2(计算技术、计算机技术)

资助基金：实验室研究项目GCIS201808

在线出版日期：2021-07-13（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：477-480