信息网络安全 ›› 2020, Vol. 20 ›› Issue (2): 30-36.doi: 10.3969/j.issn.1671-1122.2020.02.005

• • 上一篇    下一篇

基于串空间的安全协议形式化分析研究

姚萌萌1(), 唐黎1, 凌永兴1, 肖卫东2   

  1. 1.江南计算技术研究所,无锡 214063
    2.国防大学联合勤务学院,北京 100858
  • 收稿日期:2019-10-14 出版日期:2020-02-10 发布日期:2020-05-11
  • 作者简介:

    作者简介:姚萌萌(1982—),男,山东,博士研究生,主要研究方向为网络安全;唐黎(1971—),女,江苏,高级工程师,硕士,主要研究方向为信息安全;凌永兴(1965—),男,山东,高级工程师,本科,主要研究方向为信息安全;肖卫东(1964—),男,江苏,教授,硕士,主要研究方向为信息技术、网络安全、教育训练。

  • 基金资助:
    国家自然科学基金[91430214];核高基重大专项[2017ZX01028101]

Formal Analysis of Security Protocol Based on Strand Space

YAO Mengmeng1(), TANG Li1, LING Yongxing1, XIAO Weidong2   

  1. 1. Jiangnan Institute of Computing Technology, Wuxi 214063, China
    2. Joint Logistics College of National Defence University of PLA, Beijing 100858, China
  • Received:2019-10-14 Online:2020-02-10 Published:2020-05-11

摘要:

安全协议是信息安全领域的重要组成部分,随着新兴技术的快速发展,安全协议变得越来越复杂,给安全协议的形式化分析带来了挑战。近年来,基于串空间理论的形式化分析方法是一个研究热点,在安全协议分析领域得到了广泛的关注和研究,并取得了一定的成果。文章扩展了串空间理论,提出了匹配串、匹配结点、同一执行丛等概念,并基于扩展的串空间理论形式化分析了基于区块链的公平多方不可否认协议,发现了该协议的不能满足公平性的缺陷。

关键词: 串空间, 形式化分析, 安全协议, 区块链

Abstract:

Security protocols are an important component in the field of information security. With the rapid development of emerging technologies, security protocols have become more and more complex, posing a challenge to the formal analysis of security protocols. In recent years, the formal analysis method based on the strand space theory is a hot spot, and it has received attention and research in the field of security protocol analysis, and has achieved certain results. This paper extends the theory of strand space, the concepts of matching strings, matching nodes, and the same execution cluster are proposed , and formalizes the fair multi-party non-repudiation protocol based on block chain using extend strand space theory, and finds the defect the protocol can’t satisfy fairness.

Key words: strand space, formal analysis, security protocol, block chain

中图分类号: