Mechanised Verification of Distributed State-Space Algorithms for Security Protocols

Explicit model-checking (MC) is a classical solution to find flaws in a security protocol. But it is well-known that for non trivial protocols, MC may enumerate state-spaces of astronomical sizes - the famous state-space explosion problem. Distributed model checking is a solution but complex and subject to bugs: a MC can validate a model but miss an invalid state. In this paper, we focus on using a verification condition generator that takes annotated distributed algorithms and ensures their termination and correctness. We study five algorithms (one sequential and four distributed where three of them are dedicated and optimised for security protocol) of state-space construction as a first step towards mechanised verification of distributed model-checkers.