协议组合逻辑在实例化空间模型中的语义解释  

Semantic Interpretation of Protocol Compositional Logic in Instantiation Space Model

作　　者：肖茵茵[1,2] 苏开乐[2,3] 

机构地区：[1]广东技术师范学院计算机学院,广东广州510665 [2]中山大学信息科学与技术学院广东省信息安全重点实验室,广东广州510275 [3]浙江师范大学数理与信息工程学院,浙江金华321004

出　　处：《广东技术师范学院学报》2016年第2期8-19,共12页Journal of Guangdong Polytechnic Normal University

基　　金：国家自然科学基金(60903054;61379019);国家"973"重点基础研究发展计划资助项目(2010CB328103);中国博士后科学基金面上项目(2013M540704);广东高校优秀青年创新人才培育项目(LYM11085;LYM11084)资助

摘　　要：安全协议的验证是个不可判问题.为了对实例化空间逻辑ISL的语义表达能力给出理论上的衡量与评价,选择另一种实用的协议组合逻辑PCL,分析了ISL和PCL之间的关系.在此基础上,将PCL的索状空间语义模型转换为ISL的实例化空间语义模型,在实例化空间下对PCL的主要公式、定理、推导规则做了语义解释.研究表明,实例化空间能够完全表示PCL的语义,且ISL的语义表达能力强于PCL.新的模型解释使PCL更易于扩展,且使得用PCL理论验证的协议能够利用ISL的自动化验证工具SPV进行分析.The verification of protocols is an undecidable problem. In order to evaluate the semantics expressive ability of Instantiation Space Logic（ISL） theoretically, another practical protocol logic called Protocol Compositional Logic（PCL） was chosen, and the relationship between ISL and PCL was analyzed. Based on the relationship, the PCL semantic model called Cord Space was changed into the ISL semantic model, and the main formulas, axioms and inference rules of PCL were interpreted in Instantiation Space. The research shown that the Instantiation Space could express the semantics of PCL completely, and the expressive ability of ISL was stronger than that of PCL. The new interpreted PCL could be extended more easily, and those security protocols described in PCL could be verified by Security Protocol Verifier（SPV） of ISL automatically.

关 键 词：安全协议验证 实例化空间 协议组合逻辑 索状空间 语义解释 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]