文献类型：期刊文献

中文题名：一种新的安全协议验证逻辑及其串空间语义

英文题名：New Verification Logic of Security Protocols and Its Strand Space Semantics

作者：陈莉[1]

第一作者：陈莉

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

第一机构：河南财经政法大学

年份：2011

卷号：37

期号：1

起止页码：145-148

中文期刊名：计算机工程

外文期刊名：Computer Engineering

收录：CSTPCD;;Scopus;北大核心:【北大核心2008】；CSCD:【CSCD2011_2012】；

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

语种：中文

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

外文关键词：security property; strand space; logic semantics; hybrid cryptography primitives

摘要：针对典型的安全协议验证逻辑存在的问题,如安全属性验证存在局限性、对混合密码原语的处理能力不强等,提出一种新的验证逻辑,新逻辑能够验证安全协议的认证性、密钥保密性、非否认性、可追究性、公平性及原子性。现有多数验证逻辑缺乏形式化语义,而逻辑语义能够证明逻辑系统的正确性,因此给出新逻辑所含逻辑构件的串空间语义,并应用串空间模型证明了新逻辑主要推理规则的正确性。
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.