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

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

New Verification Logic of Security Protocols and Its Strand Space Semantics

Aiming at the problems of typical verification logic of security protocols, such as the limitations in verifying security properties, the lack of analysis ability of hybrid cryptography-based primitives. This paper proposes a new verification logic, which can verify almost all of the known security properties of the e-commerce protocols, such as authentication, secrecy of key, non-repudiation, accountability, fairness and atomicity. Because most of the verification logics are lack of formal semantics, and formal semantics can prove the correctness of the logic systems, the paper describes strand space semantics of the logic sentences in the new logic and proves the correctness of the main inference rules using strand space model.