基于数理逻辑的安全协议本征逻辑分析方法OA北大核心CSTPCD

This study proposes a new"security protocol analysis latent logic"(SPALL)method(also known as latent method or L-logic)based on the mathematical logic theory.In the proposed method,some new semantics related to cryptography and security protocol analysis(i.e.,cryptographic function terms,first-order predicates,and second-order predicates)are given.Moreover,twenty-nine axioms of thirteen categories are given,and predicate logic's separation and generalization rules are used to form new formulas.Thus,a new axiom system is presented as an extension of the first-order predicate system.The cryptography and security protocol background is a"particular interpretation"of the proposed system.This paper further defines a concept of"probabilistic truth",and tries to make every axiom to be a probabilistic truth under the"particular interpretation".Because the separation and generalization rule keep the probabilistic truth,every theorem is a probabilistic truth.There-fore,the reliability of the axiom system is ensured.Since clear semantics can accurately describe the premises and goals of a security protocol and briefly and effectively derive protocol security charac-teristic formula based on axioms and theorems,the protocol analysis can be presented.In this paper,the detailed semantics and axioms,as well as some practical theorems are given,and then a well-known"key establishment"protocol is analyzed as a practical instance.Compared to the"provable security"approach,the analysis results of the proposed method are brief and accurate.Furthermore,an electronic election protocol and a non-repudiation protocol are analyzed as further instances to demonstrate the advantages and wider applications of the proposed method.