|
|||||
|
|
| 图元的子句时新性 | |
| 作者单位： | 安徽建筑工业学院数理系，合肥工业大学计算机与信息学院 |
| 摘 要： | 为了给出消息子句的测试关系,选择主体角色进程演算为π演算的一个子集,以该子集刻画并发密码协议系统,事件图为其指称语义模型,由图元的前缀、非确定选择和并发合成运算得到,对于图元及其组合运算来说,图元的子句时新性质确定了主体角色消息语句的子句测试关系,且出现在图元中的消息事件满足通信关系和前驱关系约束.由图元生成的事件图涵盖了由子句测试关系构造的未知主体角色串,且通过定义图元互模拟刻画事件图的互模拟等价关系可实现并发密码协议系统安全性验证. |
| 关 键 词： | 图元 时新性 事件图 测试关系 密码协议 |
Freshness of sub-terms in meta-graphs |
|
| Authors: | Wang Huanbao Zhang Yousheng |
| Institution: | Wang Huanbao1 Zhang Yousheng2 |
| Abstract: | |
| Keywords: | meta-graph freshness event graph test relations cryptographic protocol |
| 本文献已被 CNKI 等数据库收录！ | |