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

Latent Logic Analysis Method of Security Protocol Based on Mathematical Logic

作　　者：李益发 孔雪曼 耿宇[1] 沈昌祥[2] LI Yi-Fa;KONG Xue-Man;GENG Yu;SHEN Chang-Xiang(College of Cyberspace Security,Zhengzhou University,Zhengzhou 450002,China;Naval Academy、Chinese Academy of Engineering,Beijing 100088,China)

机构地区：[1]郑州大学网络空间安全学院,郑州450002 [2]海军研究院、中国工程院,北京100088

出　　处：《密码学报（中英文）》2024年第3期588-601,共14页Journal of Cryptologic Research

基　　金：保密通信重点实验室基金课题(61421030107012102)。

摘　　要：本文提出了一种基于数理逻辑的安全协议本征逻辑分析方法—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.

关 键 词：安全协议 协议分析 BAN类逻辑 SPALL方法(SPALL逻辑) 本征逻辑 

分 类 号：TP309.7[自动化与计算机技术—计算机系统结构]