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.

Presented at:
Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, Affiliated with ETAPS 2009, York, UK, March 28-29, 2009

 Record created 2012-01-20, last modified 2018-09-13

Download fulltext

Rate this document:

Rate this document:
(Not yet reviewed)