TU Darmstadt / ULB / TUbiblio

Automated analysis of security protocols with global state

Kremer, Steve ; Künnemann, Robert (2014)
Automated analysis of security protocols with global state.
San Jose, CA, USA
doi: 10.1109/SP.2014.18
Konferenzveröffentlichung, Bibliographie

Kurzbeschreibung (Abstract)

Security APIs, key servers and protocols that need to keep the status of transactions, require to maintain a global, non-monotonic state, e.g., in the form of a database or register. However, existing automated verification tools do not support the analysis of such stateful security protocols - sometimes because of fundamental reasons, such as the encoding of the protocol as Horn clauses, which are inherently monotonic. An exception is the recent tamarin prover which allows specifying protocols as multiset rewrite (MSR) rules, a formalism expressive enough to encode state. As multiset rewriting is a "low-level" specification language with no direct support for concurrent message passing, encoding protocols correctly is a difficult and error-prone process. We propose a process calculus which is a variant of the applied pi calculus with constructs for manipulation of a global state by processes running in parallel. We show that this language can be translated to MSR rules whilst preserving all security properties expressible in a dedicated first-order logic for security properties. The translation has been implemented in a prototype tool which useqs the tamarin prover as a backend. We apply the tool to several case studies among which a simplified fragment of PKCS#11, the Yubikey security token, and an optimistic contract signing protocol.

Typ des Eintrags: Konferenzveröffentlichung
Erschienen: 2014
Autor(en): Kremer, Steve ; Künnemann, Robert
Art des Eintrags: Bibliographie
Titel: Automated analysis of security protocols with global state
Sprache: Deutsch
Publikationsjahr: Mai 2014
Verlag: IEEE Computer Society
Buchtitel: Proceedings of the 2014 IEEE Symposium on Security and Privacy
Reihe: SP '14
Veranstaltungsort: San Jose, CA, USA
DOI: 10.1109/SP.2014.18
Kurzbeschreibung (Abstract):

Security APIs, key servers and protocols that need to keep the status of transactions, require to maintain a global, non-monotonic state, e.g., in the form of a database or register. However, existing automated verification tools do not support the analysis of such stateful security protocols - sometimes because of fundamental reasons, such as the encoding of the protocol as Horn clauses, which are inherently monotonic. An exception is the recent tamarin prover which allows specifying protocols as multiset rewrite (MSR) rules, a formalism expressive enough to encode state. As multiset rewriting is a "low-level" specification language with no direct support for concurrent message passing, encoding protocols correctly is a difficult and error-prone process. We propose a process calculus which is a variant of the applied pi calculus with constructs for manipulation of a global state by processes running in parallel. We show that this language can be translated to MSR rules whilst preserving all security properties expressible in a dedicated first-order logic for security properties. The translation has been implemented in a prototype tool which useqs the tamarin prover as a backend. We apply the tool to several case studies among which a simplified fragment of PKCS#11, the Yubikey security token, and an optimistic contract signing protocol.

Freie Schlagworte: Protocols, Security, Calculus, Mathematical model, Contracts, Analytical models, Semantics
ID-Nummer: TUD-CS-2014-1110
Fachbereich(e)/-gebiet(e): Profilbereiche > Cybersicherheit (CYSEC)
Profilbereiche
Hinterlegungsdatum: 24 Aug 2017 15:54
Letzte Änderung: 15 Mai 2018 10:33
PPN:
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen