Symbolic Analysis of Identity-Based Protocols
| Autor: | David Basin, Lucca Hirschi, Ralf Sasse |
|---|---|
| Přispěvatelé: | Department of Computer Science [ETH Zürich] (D-INFK), Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Proof techniques for security protocols (PESTO), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Springer |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
Protocol (science)
Theoretical computer science Point (typography) Computer science business.industry 020206 networking & telecommunications Cryptography 0102 computer and information sciences 02 engineering and technology Cryptographic protocol 16. Peace & justice Encryption 01 natural sciences Symbolic data analysis [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] 010201 computation theory & mathematics Simple (abstract algebra) 0202 electrical engineering electronic engineering information engineering Identity (object-oriented programming) [INFO]Computer Science [cs] business |
| Zdroj: | Foundations of Security, Protocols, and Equational Reasoning Springer. Foundations of Security, Protocols, and Equational Reasoning, Springer (11565), pp.112-134, 2019, LNCS, ⟨10.1007/978-3-030-19052-1_9⟩ Foundations of Security, Protocols, and Equational Reasoning ISBN: 9783030190514 |
| DOI: | 10.1007/978-3-030-19052-1_9⟩ |
| Popis: | International audience; We show how the Tamarin tool can be used to model and reason about security protocols using identity-based cryptography, including identity-based encryption and signatures. Although such protocols involve rather different primitives than conventional public-key cryptography , we illustrate how suitable abstractions and Tamarin's support for equational theories can be used to model and analyze realistic industry protocols, either finding flaws or gaining confidence in their security with respect to different classes of adversaries. Technically, we propose two models of identity-based cryptography. First, we formalize an abstract model, based on simple equations, in which verification of realistic protocols is feasible. Second, we formalize a more precise model, leveraging Tamarin's support for bilinear pairing and exclusive-or. This model is much closer to practical realizations of identity-based cryptography, but deduction is substantially more complex. Along the way, we point out the limits of precise modeling and highlight challenges in providing support for equational reasoning. We evaluate our models on an industrial protocol case study, where we find and fix flaws. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|