Skip to Main content Skip to Navigation
Book sections

Symbolic Analysis of Identity-Based Protocols

Abstract : 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.
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/hal-02368842
Contributor : Lucca Hirschi <>
Submitted on : Monday, September 21, 2020 - 4:15:46 PM
Last modification on : Thursday, May 27, 2021 - 1:54:07 PM
Long-term archiving on: : Friday, December 4, 2020 - 9:10:21 PM

File

IDbased.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

David Basin, Lucca Hirschi, Ralf Sasse. Symbolic Analysis of Identity-Based Protocols. Springer. Foundations of Security, Protocols, and Equational Reasoning, Springer (11565), pp.112-134, 2019, LNCS, ⟨10.1007/978-3-030-19052-1_9⟩. ⟨hal-02368842⟩

Share

Metrics

Record views

128

Files downloads

130