一种基于进程代数的安全协议验证消解算法

A Reduction Algorithm Based on Process Algebra for Security Protocol Verification

安全协议本质上是分布式并发程序,可以描述为多个子进程的并发合成系统。将安全协议对应的并发合成系统抽象为一组逻辑规则,能够对安全协议无穷会话的交叠运行进行验证。本文首先给出了将安全协议基于进程代数的形式描述转化成为一组逻辑规则的方法,并提出了基于逻辑规则分类的高效逻辑程序消解算法,对安全协议认证性和保密性进行验证。

Essentially, security protocol can be considered as a set of distributed parallel programs, described as a parallel composition system including several sub-processes. We abstract this as a group of logic rules, which makes it possible to do the verification of the interleaving of infinite sessions of the security protocol. Our thesis proposes the approach to converting the process-algebra-described protocol to the horn logic rules , and proposes the high-efficiency algorithm of reduction.