针对改进型的Helsinki协议安全性问题,利用协议组合逻辑PCL对协议进行形式化分析.首先使用基于“Cords演算”的程序描述语言对协议本身进行形式化描述,然后通过协议逻辑描述协议的安全属性,最后给出性质和定理,并通过逻辑推理证明改进型Helsinki协议满足其安全要求,该协议是安全的. Aiming at the problem of the improved Helsinki protocol security, the protocol is formally analyzed by using the protocol combinatorial logic PCL.First, the protocol itself is formally described by the program description language based on “Cords calculus ”, and then the protocol logic describes the protocol At last, we give the properties and theorems, and prove that the improved Helsinki protocol satisfies its security requirements through logical reasoning. This protocol is secure.