CAJ | 학술논문

基于实例化空间逻辑理论,使用知识推理方法,在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明,并对协议进行了改进.SPV调用工业级SAT求解器,能够高效验证安伞协议是否满足CAPSL(Common Authentication Protocol Specification Language)协议规范及单层、多层认知规范.应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化,而SET协议作为当前最复杂的工业级协议,其原始文档有上千页,因此简化过程相当困难,相关研究较少,已有的一些简化模型也不够完整.因此,文章针对SET证书申请协议,给出了比以往更贴近原协议的简化模型,并详细阐述了该模型在SPV下的形式化描述及验证过程、验证结果,分析了由于协议不满足某些认知规范所带来的安全隐患,从而对协议进行改进,最后证明了改进后协议的有效性.该工作也充分说明了SPV足以处理复杂的工业级协议.
기우실례화공간라집이론,사용지식추리방법,재SPV(Security Protocol Verifier)하대완정SET증서신청협의적비밀성、인증성등안전성질진행료완전자동화증명,병대협의진행료개진.SPV조용공업급SAT구해기,능구고효험증안산협의시부만족CAPSL(Common Authentication Protocol Specification Language)협의규범급단층、다층인지규범.응용일개라집혹공구대협의진행험증수선필수대해협의진행간화,이SET협의작위당전최복잡적공업급협의,기원시문당유상천혈,인차간화과정상당곤난,상관연구교소,이유적일사간화모형야불구완정.인차,문장침대SET증서신청협의,급출료비이왕경첩근원협의적간화모형,병상세천술료해모형재SPV하적형식화묘술급험증과정、험증결과,분석료유우협의불만족모사인지규범소대래적안전은환,종이대협의진행개진,최후증명료개진후협의적유효성.해공작야충분설명료SPV족이처리복잡적공업급협의.