LDYIS: a framework for model checking security protocols We present a formalism for the automatic verification of security protocols based on multi-agent systems semantics. We give the syntax and semantics of a temporal-epistemic security-specialised logic and provide a lazy-intruder model for the protocol rules that we argue to be particularly suitable for verification purposes. We exemplify the technique by finding a (known) bug in the traditional NSPK protocol
Keywords for this software
References in zbMATH (referenced in 3 articles , 1 standard article )
Showing results 1 to 3 of 3.
- Dima, Cătălin: Non-axiomatizability for the linear temporal logic of knowledge with concrete observability (2011)
- Boureanu, Ioana; Cohen, Mika; Lomuscio, Alessio: Automatic verification of temporal-epistemic properties of cryptographic protocols (2009)
- Lomuscio, Alessio; Penczek, Wojciech: LDYIS: a framework for model checking security protocols (2008)