论文部分内容阅读
基于实例化空间逻辑理论，使用知识推理方法，在SPV（Security Protocol Verifier）下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明，并对协议进行了改进。SPV调用工业级SAT求解器，能够高效验证安全协议是否满足CAPSL（Common Authentication Protocol Specification Language）协议规范及单层、多层认知规范。应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化，而SET协议作为当前最复杂的工业级协议，其原