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