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

摘要

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