安全协议的进程代数规约到逻辑程序的自动转换

• 作者: 刘万伟 周倜 李梦君 李舟军
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 安全协议 进程代数 形式化验证 认证性 Objective Caml
• 年，卷（期）: 2006,（1）
• 所属期刊栏目: 计算机网络与安全
• 页码范围: 22-24,27
• 页数: 4页
• 分类号: TP309
• 字数: 3032字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2006.01.008

摘要

安全协议用于实现开放互连网络的安全通讯,它本质上是分布式并发程序,使用进程代数可以将其描述为角色进程的并发合成系统.使用抽象方法,安全协议角色进程并发合成模型可以转化为逻辑程序;通过计算逻辑程序的不动点,能够对安全协议无穷会话的并发交叠运行进行验证.本文基于Objective Caml语言,实现了安全协议进程代数描述到安全协议逻辑程序的自动转化.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周倜	国防科技大学计算机学院	8	33	3.0	5.0
2	李梦君	国防科技大学计算机学院	21	193	8.0	13.0
3	刘万伟	国防科技大学计算机学院	10	20	3.0	3.0
4	李舟军	国防科技大学计算机学院	31	594	10.0	24.0