基于图元的事件图生成算法

摘要：

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

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

所属期刊栏目：33

分类号：TP309(计算技术、计算机技术)

资助基金：国家自然科学基金50379003;教育部高等学校博士学科点专项科研基金20050359012;安徽省自然科学基金03042207

在线出版日期：2007-07-16（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：1-3