| 安全协议的进程代数规约到逻辑程序的自动转换 |
| |
| 引用本文： | 周倜,李梦君,刘万伟,李舟军.安全协议的进程代数规约到逻辑程序的自动转换[J].计算机工程与科学,2006,28(1):22-24. |
| |
| 作者姓名： | 周倜 李梦君 刘万伟 李舟军 |
| |
| 作者单位： | 国防科技大学计算机学院,湖南,长沙,410073 |
| |
| 基金项目： | 中国科学院资助项目;国家科技攻关项目 |
| |
| 摘 要： | 安全协议用于实现开放互连网络的安全通讯，它本质上是分布式并发程序，使用进程代数可以将其描述为角色进程的并发合成系统。使用抽象方法，安全协议角色进程并发合成模型可以转化为逻辑程序；通过计算逻辑程序的不动点，能够对安全协议无穷会话的并发交叠运行进行验证。本文基于Objective Caml语言，实现了安全协议进程代数描述述到安全协议逻辑程序的自动转化。
|
| 关 键 词： | 安全协议 进程代数 形式化验证 认证性 Objective Canal |
| 文章编号： | 1007-130X(2006)01-0022-03 |
| 修稿时间： | 2004年11月12 |
Auto-Transformation of the Process Algebra Specification of Security Protocols into Logic Programs |
| |
| ZHOU Ti,LI Meng-jun,LIU Wan-wei,LI Zhou-jun.Auto-Transformation of the Process Algebra Specification of Security Protocols into Logic Programs[J].Computer Engineering & Science,2006,28(1):22-24. |
| |
| Authors: | ZHOU Ti LI Meng-jun LIU Wan-wei LI Zhou-jun |
| |
| Abstract: | |
| |
| Keywords: | Objective Caml |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与科学》浏览原始摘要信息 |
|
点击此处可从《计算机工程与科学》下载全文 |
|
