Tamarin: Verification of Large-Scale, Real-World, Cryptographic Protocols

Autor: Basin, David, Cremers, Cas, Dreier, Jannik, Sasse, Ralf
Přispěvatelé: Institute of Information Security [ETH Zürich], Department of Computer Science [ETH Zürich] (D-INFK), Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich)- Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich), Helmholtz Center for Information Security [Saarbrücken] (CISPA), Proof techniques for security protocols (PESTO), Inria Nancy - Grand Est, 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), 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)-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)
Rok vydání: 2022
Předmět:
Zdroj: IEEE Security and Privacy Magazine
IEEE Security and Privacy Magazine, In press, ⟨10.1109/msec.2022.3154689⟩
ISSN: 1558-4046
1540-7993
Popis: International audience; Tamarin is a mature, state-of-the-art tool for cryptographic protocol verification. We introduce Tamarin and survey some of the larger, tour-de-force results achieved with it. We also show how Tamarin can formalize a wide range of protocols, adversary models, and properties, and scale to substantial, real-world, verification problems.
Databáze: OpenAIRE
Externí odkaz: