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

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

Improvement and formal proof on protocol Otway-Rees

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.