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

关键词：安全协议 进程代数 形式化验证 认证性 objective 

单位：国防科技大学计算机学院; 湖南长沙410073