Update publications.bib

publications.bib

@@ -1832,7 +1832,32 @@ author    = {Emanuele D'Osualdo and
 title     = {(Submitted) TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs},
 year      = {2020},
 }
-
+@InProceedings{DOsualdoS2020Decidable,
+author    = {Emanuele D'Osualdo and
+            Felix Stutz},
+editor    = {Igor Konnov and
+               Laura Kov{\'{a}}cs},
+title     = {Decidable Inductive Invariants for Verification of Cryptographic Protocols
+               with Unbounded Sessions},
+booktitle = {31st International Conference on Concurrency Theory, {CONCUR} 2020,
+               September 1-4, 2020, Vienna, Austria (Virtual Conference)},
+series    = {LIPIcs},
+volume    = {171},
+pages     = {31:1--31:23},
+publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
+year      = {2020},
+url       = {https://doi.org/10.4230/LIPIcs.CONCUR.2020.31},
+doi       = {10.4230/LIPIcs.CONCUR.2020.31},
+abstract  = {We develop a theory of decidable inductive invariants for an infinite-state variant of the Applied
+π-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.},
+}
 
 @Comment{jabref-meta: databaseType:bibtex;}