DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2020.31

Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions

Authors: Emanuele D'Osualdo and Felix Stutz

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract

We develop a theory of decidable inductive invariants for an infinite-state variant of the Applied πcalc, 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.

Cite as

Emanuele D'Osualdo and Felix Stutz. Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 31:1-31:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{dosualdo_et_al:LIPIcs.CONCUR.2020.31,
  author =	{D'Osualdo, Emanuele and Stutz, Felix},
  title =	{{Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{31:1--31:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.31},
  URN =		{urn:nbn:de:0030-drops-128433},
  doi =		{10.4230/LIPIcs.CONCUR.2020.31},
  annote =	{Keywords: Security Protocols, Infinite-State Verification, Ideal Completions for WSTS}
}

Search Results

Documents authored by D'Osualdo, Emanuele

Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions

Abstract

Cite as

Thanks for your feedback!

Could not send message