密码学报2024，Vol.11Issue(3)：588-601,14.DOI:10.13868/j.cnki.jcr.000696
基于数理逻辑的安全协议本征逻辑分析方法
Latent Logic Analysis Method of Security Protocol Based on Mathematical Logic
摘要
Abstract
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逻辑)/本征逻辑Key words
security protocol/protocol analysis/BAN-like logic/SPALL method/latent logic分类
信息技术与安全科学引用本文复制引用
李益发,孔雪曼,耿宇,沈昌祥..基于数理逻辑的安全协议本征逻辑分析方法[J].密码学报,2024,11(3):588-601,14.基金项目
保密通信重点实验室基金课题(61421030107012102)Key Laboratory of Secure Communications Fund Project(61421030107012102) （61421030107012102）
