Automatic Verification of Temporal-Epistemic Properties of Cryptographic Protocols

We present a technique for automatically verifying cryptographic protocols specified in the mainstream specification language CAPSL. We define a translation from CAPSL models into interpreted systems, a popular semantics for temporal-epistemic logic, and rewrite CAPSL goals as temporal-epistemic specifications. We present a compiler that implements this translation. The compiler links to the symbolic model checker MCMAS. We evaluate the technique on protocols in the Clark-Jacobs library and in the SPORE repository against custom secrecy and authentication requirements.


Published in:
Journal of Applied Non-classical Logics, 19, 4, 463-487
Year:
2009
Keywords:
Laboratories:




 Record created 2012-01-20, last modified 2018-03-17

n/a:
Download fulltext
PDF

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)