论文部分内容阅读
在以Lu＆Smolka对SET协议支付过程的简化模型为研究对象的情况下，进行形式化建模和有限状态机模型。同时应用CTL对相应的安全性质进行形式描述，并在网络环境被入侵者控制的假设下，利用SMV分析了协议的认证性、保密性和完整性，发现攻击并对该攻击所产生的影响进行了讨论。最后修改其协议模型对改进后的协议进行分析和检验，说明了SET协议独具特色的双重签名在整个协议运行中至关重要。