实例化空间:一种新的安全协议验证逻辑的语义模型

Instantiation Space: A New Model for Security Protocol Logic

给出了一个称为“实例化空间(instantiation space)”的安全协议验证逻辑的语义模型.该语义模型是建立在一种自然的加密信息交换(cryptographical message exchange)模型上的.在此语义模型基础上,文章提出了一系列与安全属性相关的验证公理,由此可以证明它们在此语义模型下的正确性.更重要的是,在此语义下的公理集在算法上是完全可以实现的,其对应的工具SPV(Security Protocol Verifier)已经开发成功,并且可以验证复杂的协议.在这套安全协议验证模型理论下,可以很方便地处理包括公钥、私钥、共享密钥和Hash函数组成的复杂信息格式.而且,在此语义基础上的公理集是纯命题逻辑的,因此所需要的验证目标可以很方便地转化成可满足性问题(SAT),从而可以利用工业上快速高效的SAT求解器实现.

The authors present a new model of security protocol logics, which is called Instantiation Space. This model is formally well grounded, based on the so-called Cryptographical Message Exchange（CME） model. A set of interesting axioms （security properties） can be shown to be sound within the Instantiation Space model. It is worth noting that, this set of axioms is algorithmic manageable, and hence a new Security Protocol Verifier （SPV） can be designed and implemented, particularly focused on automatic verification of complex protocols. The presented approach to security protocol verification is flexible enough to deal with complex message formats with arbitrarily nested encryptions by public, private, shared and hash keys as well as freshly generated keys. Moreover, the set of axioms for a protocol the authors generated based on Instantiation Space model is in propositional logic; for a lot of concerned security properties the verification problems can thus be formulated as satisfiability ones, which can be solved by efficient modern SAT solvers.