Bitte benutzen Sie diese Kennung, um auf die Ressource zu verweisen:
http://dx.doi.org/10.18419/opus-13472
Langanzeige der Metadaten
DC Element | Wert | Sprache |
---|---|---|
dc.contributor.author | Bhargavan, Karthikeyan | - |
dc.contributor.author | Bichhawat, Abhishek | - |
dc.contributor.author | Hosseyni, Pedram | - |
dc.contributor.author | Küsters, Ralf | - |
dc.contributor.author | Pruiksma, Klaas | - |
dc.contributor.author | Schmitz, Guido | - |
dc.contributor.author | Waldmann, Clara | - |
dc.contributor.author | Würtele, Tim | - |
dc.date.accessioned | 2023-09-08T12:49:26Z | - |
dc.date.available | 2023-09-08T12:49:26Z | - |
dc.date.issued | 2023 | de |
dc.identifier.uri | http://nbn-resolving.de/urn:nbn:de:bsz:93-opus-ds-134914 | de |
dc.identifier.uri | http://elib.uni-stuttgart.de/handle/11682/13491 | - |
dc.identifier.uri | http://dx.doi.org/10.18419/opus-13472 | - |
dc.description.abstract | While cryptographic protocols are often analyzed in isolation, they are typically deployed within a stack of protocols, where each layer relies on the security guarantees provided by the protocol layer below it, and in turn provides its own security functionality to the layer above. Formally analyzing the whole stack in one go is infeasible even for semi-automated verification tools, and impossible for pen-and-paper proofs. The DY* protocol verification framework offers a modular and scalable technique that can reason about large protocols, specified as a set of F* modules. However, it does not support the compositional verification of layered protocols since it treats the global security invariants monolithically. In this paper, we extend DY* with a new methodology that allows analysts to modularly analyze each layer in a way that compose to provide security for a protocol stack. Importantly, our technique allows a layer to be replaced by another implementation, without affecting the proofs of other layers. We demonstrate this methodology on two case studies. We also present a verified library of generic authenticated and confidential communication patterns that can be used in future protocol analyses and is of independent interest. | en |
dc.language.iso | en | de |
dc.rights | info:eu-repo/semantics/openAccess | de |
dc.subject.ddc | 004 | de |
dc.title | Layered symbolic security analysis in DY* | en |
dc.type | conferenceObject | de |
ubs.bemerkung.extern | Technical report corresponding to a paper published at ESORICS 2023 | de |
ubs.fakultaet | Informatik, Elektrotechnik und Informationstechnik | de |
ubs.fakultaet | Fakultätsübergreifend / Sonstige Einrichtung | de |
ubs.institut | Institut für Informationssicherheit | de |
ubs.institut | Fakultätsübergreifend / Sonstige Einrichtung | de |
ubs.konferenzname | European Symposium on Research in Computer Security (28th, 2023, Den Haag) | de |
ubs.publikation.noppn | yes | de |
ubs.publikation.typ | Konferenzbeitrag | de |
Enthalten in den Sammlungen: | 05 Fakultät Informatik, Elektrotechnik und Informationstechnik |
Dateien zu dieser Ressource:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
Layered_Symbolic_Security_Analysis_in_DYstar_TR.pdf | 465 kB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repositorium sind urheberrechtlich geschützt.