Current browse context:
cs.LO
Change to browse by:
References & Citations
Computer Science > Logic in Computer Science
Title: Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions
(Submitted on 13 Nov 2019 (v1), last revised 19 Jul 2020 (this version, v2))
Abstract: 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.
Submission history
From: Emanuele D'Osualdo [view email][v1] Wed, 13 Nov 2019 12:45:28 GMT (83kb,D)
[v2] Sun, 19 Jul 2020 09:15:53 GMT (96kb,D)
Link back to: arXiv, form interface, contact.