论文部分内容阅读
基于卿-周逻辑给出了一些新的逻辑推理规则，并提出了一种扩展的通信有限状态自动机，用于分析电子商务协议的安全性质。该方法可描述协议参与者的行为与知识，且无需人为地引入初始假设。对扩展模型抽象并修改后，还可验证其它一些与加密、签名消息无关的性质。利用该方法分析了匿名可恢复的公平交换协议，发现其满足有效性、公平性、可追究性，但不满足匿名性，并用UPPAAL验证了协议的公平性、活性与时效性等。