基于逻辑程序的安全协议验证

• 作者: 李梦君 李舟军 陈火旺
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 安全协议 逻辑程序 不动点 验证策略
• 年，卷（期）: 2004,（10）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 1361-1368
• 页数: 8页
• 分类号: TP309
• 字数: 9022字
• 语种: 中文
• DOI: 10.3321/j.issn:0254-4164.2004.10.008

摘要

安全协议本质上是分布式并发程序,可以自然地描述为多个子进程的并发合成系统.将安全协议对应的并发合成系统抽象为逻辑程序进行消解,能够对安全协议无穷多个会话的交叠运行进行验证.该文提出了安全协议逻辑程序中逻辑规则的一个分类方法,基于该分类方法提出了安全协议逻辑程序不动点的迭代计算方法.逻辑规则的分类优化了安全协议逻辑程序不动点的迭代计算和安全性质验证过程中的计算.由于安全协议逻辑程序不动点迭代计算过程不一定终止,文中提出了每进行k≥1步安全协议逻辑程序不动点迭代计算验证一次安全性质的验证策略.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈火旺	国防科学技术大学计算机学院	53	2116	23.0	45.0
2	李舟军	国防科学技术大学计算机学院	17	339	7.0	17.0
3	李梦君	国防科学技术大学计算机学院	16	294	7.0	16.0