Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions
This work addresses the challenge of automatic verification for cryptographic protocols, offering a decidable solution for a broader class than prior methods, though it is incremental in extending existing theory.
The paper tackles the undecidable problem of verifying stateful cryptographic protocols with unbounded sessions by introducing depth-bounded protocols and a decidable procedure to check inductive invariants, enabling automatic verification with a prototype implementation tested on textbook examples.
We develop a theory of decidable inductive invariants for an infinite-state variant of the Applied pi-calculus, with applications to automatic verification of stateful cryptographic protocols with unbounded sessions/nonces. Since the problem is undecidable in general, we introduce depth-bounded protocols, a strict generalisation of a class from the literature, for which our decidable analysis is sound and complete. Our core contribution is a procedure to check that an invariant is inductive, which implies that every reachable configuration satisfies it. Our invariants can capture security properties like secrecy, can be inferred automatically, and represent an independently checkable certificate of correctness. We provide a prototype implementation and we report on its performance on some textbook examples.