spi演算证明协议非可否认性

spi演算以进程代数理论作为基础,适合多轮并发条件下安全协议的证明。通过在spi系统中引入消息起源测试成功表示了签名消息的安全语义,并在此基础上验证了ZG协议的非可否认性,扩展了spi演算在安全协议证明中的应用范围。