Compilation Method for the Verification of Temporal-Epistemic Properties of Cryptographic Protocols

We present a technique for automatically verifying cryptographic protocols specified in the mainstream specification language CAPSL. Our work is based on model checking multi-agent systems against properties given in AI logics. We present PC2IS, a compiler from CAPSL to ISPL, the input language of MCMAS, a symbolic model checker for MAS. The technique also reduces automatically the state space to be considered by the model checker, thereby maximising the number of protocols and sessions that can be verified. We evaluate the technique on protocols in the Clark-Jacobs library against custom secrecy and authentication requirements as well as against more advanced properties that are expressible in this epistemic-based approach