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