摘要： 与单轮运行情形不同，多轮并发运行的密码协议存在更为复杂的安全性问题。并发运行密码协议的形式化分析对象包括密码协议的多轮并发运行和多个密码协议的并发运行两种情形，且二者具有统一的形式化模型。基于扩展的串空间模型和Spi演算理论，提出用于并发运行密码协议安全属性验证的事件图模型。图元是事件图的构造单元，它满足消息事件之间的通信关系和前驱关系约束以及消息语句的新鲜性约束。定义消息事件之间、图元之间以及消息事件和图元之间的前缀、组合和选择运算，并给出事件图生成算法。

关键词: 密码协议, 事件图, 形式化模型, 图元

Abstract: There are lots of complex security problems in the cryptographic protocols in lots of runs, which are not different from one run. The objects of formal analysis for cryptographic protocols in a concurrent way include the two ones: a cryptographic protocol in lots of runs and cryptographic protocols in a concurrent way. The above-mentioned objects are provided with the unified formal model. The event graph model is introduced based on the extended model of strand space and Spi calculus. It is a formal model for proving the safety properties of the cryptographic protocols in a concurrent way correctly. The meta-graph is a unit for composing event graphs. It meets all the restrictions in the communication and causal predecessor relation between events, and in the freshness of terms. The prefix, parallel composition, and choice operation among events and meta-graphs respectively are defined, and the meta-graph-based algorithms for composing event graphs are proposed.

Key words: Cryptographic protocol, Event graph, Formal model, Meta-graph

中图分类号: 

• TP309