一种新的安全协议验证逻辑及其串空间语义

针对典型的安全协议验证逻辑存在的问题,如安全属性验证存在局限性、对混合密码原语的处理能力不强等,提出一种新的验证逻辑,新逻辑能够验证安全协议的认证性、密钥保密性、非否认性、可追究性、公平性及原子性。现有多数验证逻辑缺乏形式化语义,而逻辑语义能够证明逻辑系统的正确性,因此给出新逻辑所含逻辑构件的串空间语义,并应用串空间模型证明了新逻辑主要推理规则的正确性。

一种分析电子商务安全协议的新逻辑

针对典型电子商务安全协议逻辑分析方法存在的问题,如安全属性分析存在局限性、缺乏形式化语义、对混合密码原语的处理能力不强等,提出了一种新的逻辑分析方法。新逻辑能够分析电子商务安全协议的认证性、密钥保密性、非否认性、可追究性、公平性及原子性。以匿名电子现金支付协议ISI作为分析实例,证明了新逻辑方法的有效性。分析找出了该协议的安全漏洞和缺陷:不满足商家的非否认性、密钥保密性、可追究性、公平性以及原子性,客户面临商家恶意欺骗的潜在威胁。