Publikation: Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions
Lade...
Dateien
Datum
2020
Autor:innen
Stutz, Felix
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
DOI (zitierfähiger Link)
Internationale Patentnummer
Link zur Lizenz
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Bookpart
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published
Erschienen in
KONNOV, Igor, Hrsg., Laura KOVÁCS, Hrsg.. 31st International Conference on Concurrency Theory (CONCUR 2020). Wadern: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, 31. Leibniz International Proceedings in Informatics (LIPIcs). 171. ISBN 978-3-95977-160-3. Verfügbar unter: doi: 10.4230/LIPIcs.CONCUR.2020.31
Zusammenfassung
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.
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Security Protocols, Infinite-State Verification, Ideal Completions for WSTS
Konferenz
31st International Conference on Concurrency Theory (CONCUR 2020), 1. Sept. 2020 - 4. Sept. 2020, Vienna, Austria
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690
D'OSUALDO, Emanuele, Felix STUTZ, 2020. Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions. 31st International Conference on Concurrency Theory (CONCUR 2020). Vienna, Austria, 1. Sept. 2020 - 4. Sept. 2020. In: KONNOV, Igor, Hrsg., Laura KOVÁCS, Hrsg.. 31st International Conference on Concurrency Theory (CONCUR 2020). Wadern: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020, 31. Leibniz International Proceedings in Informatics (LIPIcs). 171. ISBN 978-3-95977-160-3. Verfügbar unter: doi: 10.4230/LIPIcs.CONCUR.2020.31BibTex
@inproceedings{DOsualdo2020-08-26Decid-71007,
year={2020},
doi={10.4230/LIPIcs.CONCUR.2020.31},
title={Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions},
number={171},
isbn={978-3-95977-160-3},
publisher={Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
address={Wadern},
series={Leibniz International Proceedings in Informatics (LIPIcs)},
booktitle={31st International Conference on Concurrency Theory (CONCUR 2020)},
editor={Konnov, Igor and Kovács, Laura},
author={D'Osualdo, Emanuele and Stutz, Felix},
note={Article Number: 31}
}RDF
<rdf:RDF
xmlns:dcterms="http://purl.org/dc/terms/"
xmlns:dc="http://purl.org/dc/elements/1.1/"
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
xmlns:bibo="http://purl.org/ontology/bibo/"
xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
xmlns:foaf="http://xmlns.com/foaf/0.1/"
xmlns:void="http://rdfs.org/ns/void#"
xmlns:xsd="http://www.w3.org/2001/XMLSchema#" >
<rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/71007">
<void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
<dcterms:title>Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions</dcterms:title>
<dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dc:rights>terms-of-use</dc:rights>
<dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dcterms:issued>2020-08-26</dcterms:issued>
<dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
<dc:creator>D'Osualdo, Emanuele</dc:creator>
<dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/71007/4/DOsualdo_2-jokevofx1kph5.pdf"/>
<dc:language>eng</dc:language>
<dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-10-18T07:41:41Z</dcterms:available>
<dc:contributor>Stutz, Felix</dc:contributor>
<bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/71007"/>
<dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-10-18T07:41:41Z</dc:date>
<foaf:homepage rdf:resource="http://localhost:8080/"/>
<dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/71007/4/DOsualdo_2-jokevofx1kph5.pdf"/>
<dc:creator>Stutz, Felix</dc:creator>
<dc:contributor>D'Osualdo, Emanuele</dc:contributor>
<dcterms: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.</dcterms:abstract>
</rdf:Description>
</rdf:RDF>Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Prüfungsdatum der Dissertation
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Nein
