基于数理逻辑的安全协议本征逻辑分析方法

Latent Logic Analysis Method of Security Protocol Based on Mathematical Logic

本文提出了一种基于数理逻辑的安全协议本征逻辑分析方法—SPALL方法.该方法在一阶谓词逻辑的基础上,增加了基于密码学的若干新语义,包括新的密码函数项、与密码学和安全协议分析相关的一阶谓词和二阶谓词等,并给出了十三类二十九条公理,仍使用谓词逻辑的分离规则和概括规则,形成新的安全协议分析系统,称为本征(latent)逻辑系统(也称本征逻辑或L逻辑).该系统是一阶谓词系统的扩充,以密码学和安全协议为“特定解释”,并定义了“概率真”的概念,力求每条公理在“特定解释”下是概率真的,而分离和概括规则又能保证从概率真演绎出概率真,从而使每条定理都概率真,以保证公理系统的可靠性.清晰的语义可以精确描述安全协议的前提与目标,基于公理和定理的协议分析,可简洁有效地推导出协议自身具有的安全特性.本文给出了详细的语义和公理,以及若干实用定理,然后对著名的密钥建立协议进行了详细分析,并对比了可证安全方法的分析结果,展示了本文方法的优势.此外还分析了电子选举协议和非否认协议,展示了本文方法有着广泛的适用范围.

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.