一种新的安全协议验证逻辑及其串空间语义  

New Verification Logic of Security Protocols and Its Strand Space Semantics

作　　者：陈莉[1] 

机构地区：[1]河南财经学院计算中心

出　　处：《计算机工程》2011年第1期145-148,共4页Computer Engineering

基　　金：国家"863"计划基金资助项目(2007AA01Z471);国家自然科学基金资助项目(60473021);河南省科技攻关计划基金资助重点项目(072102210029);河南省科技攻关计划基金资助项目(0624260017)

摘　　要：针对典型的安全协议验证逻辑存在的问题,如安全属性验证存在局限性、对混合密码原语的处理能力不强等,提出一种新的验证逻辑,新逻辑能够验证安全协议的认证性、密钥保密性、非否认性、可追究性、公平性及原子性。现有多数验证逻辑缺乏形式化语义,而逻辑语义能够证明逻辑系统的正确性,因此给出新逻辑所含逻辑构件的串空间语义,并应用串空间模型证明了新逻辑主要推理规则的正确性。Aiming at the problems of typical verification logic of security protocols, such as the limitations in verifying security properties, the lack of analysis ability of hybrid cryptography-based primitives. This paper proposes a new verification logic, which can verify almost all of the known security properties of the e-commerce protocols, such as authentication, secrecy of key, non-repudiation, accountability, fairness and atomicity. Because most of the verification logics are lack of formal semantics, and formal semantics can prove the correctness of the logic systems, the paper describes strand space semantics of the logic sentences in the new logic and proves the correctness of the main inference rules using strand space model.

关 键 词：安全属性 串空间 逻辑语义 混合密码原语 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]