@@ -8,4 +8,4 @@ The paper explores the limits of what security properties can be proven by autom
In the paper, they 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, the authors introduce depth-bounded protocols, a strict generalisation of a class from the literature, for which our decidable analysis is sound and complete. Their core contribution is a procedure to check that an invariant is inductive, which implies that every reachable configuration satisfies it. Their invariants can capture security properties like secrecy, can be inferred automatically, and represent an independently checkable certificate of correctness. They also provide a prototype implementation and report on its performance on some textbook examples. The [extended technical report](https://arxiv.org/abs/1911.05430) is also available on [this link](https://arxiv.org/abs/1911.05430).
CONCUR 2020, the [31st International Conference on Concurrency Theory](https://drops.dagstuhl.de/opus/portals/lipics/index.php?semnr=16161) will take place online on 1-4 September2020.
CONCUR 2020, the [31st International Conference on Concurrency Theory](https://drops.dagstuhl.de/opus/portals/lipics/index.php?semnr=16161) will take place online on 1-4 September2020.
