LI Yuan1, JIANG Jian-guo1, WANG Huan-bao2. Formal analysis of non-repudiation protocol by spi[J]. 2009, 30(5): 94-98.DOI:
spi演算证明协议非可否认性
摘要
spi演算以进程代数理论作为基础
适合多轮并发条件下安全协议的证明。通过在spi系统中引入消息起源测试成功表示了签名消息的安全语义
并在此基础上验证了ZG协议的非可否认性
扩展了spi演算在安全协议证明中的应用范围。
Abstract
spi calculus
which was based on the theorems of process algebra
was fit for the proof of concurrent protocol execution. Message origination test was put up and the semantics of message sign operation was successfully expressed base on the test
at last
the non-repudiation protocol ZG was proved so as to prove the validity of the method.