Computational Logical Verification Method for Cryptographic Protocols

基于协议逻辑（BPL）是一阶逻辑的变体，用于证明密码协议的正确性。这个扩展的系统是从BPL获得的，通过增加一些计算方面的密码学和声音的计算语义。通过对Needham-Schroeder协议等协议的保密性证明，证明了该系统的有效性。

We developed an extended inference system based on Based Protocol Logic (BPL), a variant of first order logic for proving correctness of cryptographic protocols. This extended system was obtained from BPL by adding some computational aspects of cryptography and sound with respect to a computational semantics. We also demonstrated the usefulness of this system by proving secrecy property of some protocols, such as Needham-Schroeder protocol.