Abstract: This paper develops a technique by introducing probabilistic polynomial-time processes for analyzing security protocols, because of the limitations of the Spi calculus. The technique is an improvement of the Spi calculus. Protocol adversaries may be any probabilistic polynomial-time processes in the technique, and security may be expressed in terms of observational equivalence. By analyzing a protocol based on ElGamal encryption and Diffie-Hellman key exchange, it demonstrates the analysis capability of the technique for protocol security.

Key words: process algebra, probabilistic process, probabilistic observational equivalence, security protocols analysis

摘要： 针对Spi演算在安全协议分析中存在的局限性，通过引入概率多项式时间进程，提出一个分析安全协议的新方法。该方法是对Spi演算的改进，在该方法中攻击者是概率多项式时间进程，协议的安全性用概率可观察等价性表示。通过对一个基于ElGamal加密和Diffie-Hellman的密钥交换协议分析，证明了该方法的可行性和有效性。

关键词: 进程代数, 概率进程, 概率可观察等价性, 安全协议分析

CLC Number: 

• TP309