摘要
安全协议用于实现开放互连网络的安全通讯,它本质上是分布式并发程序,使用进程代数可以将其描述为角色进程的并发合成系统。使用抽象方法,安全协议角色进程并发合成模型可以转化为逻辑程序;通过计算逻辑程序的不动点,能够对安全协议无穷会话的并发交叠运行进行验证。本文基于Objective Caml语言,实现了安全协议进程代数描述到安全协议逻辑程序的自动转化。
Security protocols are used to provide secure communications over open network, which are essentially concurrent programs in distributed systems, and can be described as a parallel composition system of multiple role-processes by process algebra By using abstract methods, the security protocols＇ process model can be transformed into a logic program. By computing the fixedpoint of the logic program, we can verify the parallel interleaved operations of the security protocols＇ infinite sessions. This paper uses the Objective Carol language, and automatically translates the description of process algebra for Security protocols into relative logic programs.
出处
《计算机工程与科学》
CSCD
2006年第1期22-24,27,共4页
Computer Engineering & Science
基金
国家自然科学基金资助项目(90104026
60073001
60473057)
国家863计划资助项目(2002AA144040)
