Semantic Interpretation of Protocol Compositional Logic in Instantiation Space Model
Xiao Yin-yi · Journal of Guangdong Polytechnic Normal University · 2016
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.