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

摘要

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