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

摘要

安全协议的验证是个不可判问题.为了对实例化空间逻辑ISL的语义表达能力给出理论上的衡量与评价,选择另一种实用的协议组合逻辑PCL,分析了ISL和PCL之间的关系.在此基础上,将PCL的索状空间语义模型转换为ISL的实例化空间语义模型,在实例化空间下对PCL的主要公式、定理、推导规则做了语义解释.研究表明,实例化空间能够完全表示PCL的语义,且ISL的语义表达能力强于PCL.新的模型解释使PCL更易于扩展,且使得用PCL理论验证的协议能够利用ISL的自动化验证工具SPV进行分析.