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

Formal Analysis of Security Protocol Based on Strand Space

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

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.