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