This paper proposes a logic for verifying security protocols in the computational model ,which can describe the computation and communication actions precisely .We present a cryptographically sound proof system on the logic and can formalize the various security properties for encryption algorithms directly .During the research ,several unsoundness of the formalization with the computational protocol compositional logic in prior work is discovered ,and corresponding solutions are proposed .By proving the security properties for the Needham-Schroeder-Lowe protocol ,the power of the logic is demonstrated .Being different from most of the current verification approaches ,this logic reasons about the security of protocols from the security of cryptographic algorithms forwardly ,and is both easy to use and cryptographically sound .%提出了一个基于计算语义的安全协议验证逻辑，能准确描述安全协议中的各种计算行为和通信行为。设计了基于该逻辑的证明系统，能对密码学中常用加密算法的各类安全属性规范直接描述，具有密码学可靠性。发现了计算协议组合逻辑在加密算法安全性建模时存在的不可靠性，并提出了解决方法。通过对Needham-Schroeder-Lowe协议安全性的证明，验证了逻辑的证明能力。与大部分验证方法不同的是，本逻辑属于由密码学算法安全性到协议安全性的正向推理方法，兼具符号方法的易用性和计算方法的可靠性。
展开▼
