图元的子句时新性
为了给出消息子句的测试关系,选择主体角色进程演算为π演算的一个子集,以该子集刻画并发密码协议系统,事件图为其指称语义模型,由图元的前缀、非确定选择和并发合成运算得到,对于图元及其组合运算来说,图元的子句时新性质确定了主体角色消息语句的子句测试关系,且出现在图元中的消息事件满足通信关系和前驱关系约束.由图元生成的事件图涵盖了由子句测试关系构造的未知主体角色串,且通过定义图元互模拟刻画事件图的互模拟等价关系可实现并发密码协议系统安全性验证.
图元 子句时新性 事件图 子句测试关系 密码协议
王焕宝 张佑生
安徽建筑工业学院数理系,合肥 230022 合肥工业大学计算机与信息学院,合肥 230009
国内会议
南京
中文
25-27
2008-11-10（万方平台首次上网日期，不代表论文的发表时间）