计算机工程 ›› 2011, Vol. 37 ›› Issue (01): 145-148.doi: 10.3969/j.issn.1000-3428.2011.01.050

• 安全技术 • 上一篇    下一篇

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

陈 莉   

  1. (河南财经学院计算中心,郑州 450002)
  • 出版日期:2011-01-05 发布日期:2010-12-31
  • 作者简介:陈 莉(1968-),女,副教授、博士,主研方向:信息安全,安全协议,电子商务
  • 基金项目:
    国家“863”计划基金资助项目(2007AA01Z471);国家自然科学基金资助项目(60473021);河南省科技攻关计划基金资助重点项目(072102210029);河南省科技攻关计划基金资助项目(062426 0017)

New Verification Logic of Security Protocols and Its Strand Space Semantics

CHEN Li   

  1. (Computer Center, Henan University of Finance and Economics, Zhengzhou 450002, China)
  • Online:2011-01-05 Published:2010-12-31

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

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

Abstract: 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.

Key words: security property, strand space, logic semantics, hybrid cryptography primitives

中图分类号: