A General Approach to the Verification of Cryptographic Protocols Using Answer Set Programming

摘要

We introduce a general approach to cryptographic protocol verification based on answer set programming. In our approach, cryptographic protocols are represented as extended logic programs where the answer sets correspond to traces of protocol runs. Using queries, we can find attacks on a protocol by finding the answer sets for the corresponding logic program. Our encoding is modular, with different modules representing the message passing environment, the protocol structure and the intruder model. We can easily tailor each module to suit a specific application, while keeping the rest of the encoding constant. As such, our approach is more flexible and elaboration tolerant than related formalizations. The present system is intended as a first step towards the development of a compiler from protocol specifications to executable programs; such a compiler would make verification a completely automated process. This work is also part of a larger project in which we are exploring the advantages of explicit, declarative representations of protocol verification problems.