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

• 作者: 张佑生 王焕宝
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 密码协议 事件图 形式化模型 图元
• 年，卷（期）: 2007,（12）
• 所属期刊栏目: 博士论文
• 页码范围: 1-3
• 页数: 3页
• 分类号: TP309
• 字数: 5339字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2007.12.001

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张佑生	合肥工业大学计算机与信息学院	135	1269	19.0	29.0
2	王焕宝	安徽建筑工业学院数理系	19	48	4.0	6.0