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 (this version), latest version 19 Jul 2020 (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 in the presence of unbounded sessions any trace property becomes undecidable, we focus on (i) depth-bounded protocols, a generalisation of a class of infinite-state protocols proposed by D'Osualdo, Ong and Tiu; and (ii) downward-closed properties, which include many security properties such as absence of leaks of secrets.
We study the structure of depth-bounded protocols within the framework of ideal completions for well-structured transition systems. Our main contribution is a class of expressions, called limits, that are shown sound and complete for representing infinite downward-closed sets of configurations of depth-bounded protocols. We provide direct algorithms to prove that a given limit is an inductive invariant for a protocol. Inductive invariants of this form can be inferred, and represent an independently checkable certificate of correctness. To evaluate whether the approach is viable, we provide a prototype implementation and we report on its performance on some illustrative 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.