New Verification Logic of Security Protocols and Its Strand Space Semantics
Chen Li · Jisuanji gongcheng · 2011
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.