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 securityspecialised 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.

• Type: Journal
• Year: 2008
• Where: FUIN
• Authors: Alessio Lomuscio, Wojciech Penczek
• Keywords: Automatic Verification, FUIN 2008, Multi-agent Systems Semantics, Temporal-epistemic Securityspecialised Logic