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

Formal Analysis of Security Protocol Based on Strand Space

作　　者：姚萌萌[1] 唐黎[1] 凌永兴[1] 肖卫东 YAO Mengmeng;TANG Li;LING Yongxing;XIAO Weidong(Jiangnan Institute of Computing Technology,Wuxi 214063,China;Joint Logistics College of National Defence University of PLA,Beijing 10085&China)

机构地区：[1]江南计算技术研究所,无锡214063 [2]国防大学联合勤务学院,北京100858

出　　处：《信息网络安全》2020年第2期30-36,共7页Netinfo Security

基　　金：国家自然科学基金[91430214];核高基重大专项[2017ZX01028101]。

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

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]