Add Spotlight Tamarin Prover

_spotlights/tamarin.md

+---
+layout: spotlight
+
+###############################################################################
+# Template for Software spotlights
+###############################################################################
+# Templates starting with a _, e.g. "_template.md" will not be integrated into
+# the spotlights.
+#
+# Optional settings can be left empty.
+
+# -----------------------------------------------------------------------------
+# Properties for spotlights list page
+# -----------------------------------------------------------------------------
+
+# The name of the software
+name: Tamarin Prover
+
+# The date when the software was added to the spotlights YYYY-MM-DD
+date_added: 2022-10-07
+
+# Small preview image shown at the spotlights list page.
+# Note: the path is relative to /assets/img/spotlights/
+preview_image: tamarin/tamarin.png
+
+# One or two sentences describing the software
+excerpt: > 
+    The Tamarin Prover is a state-of-the-art tool for the
+    analysis of security protocols, which underpin the security of
+    modern distributed computing; Tamarin has been used in analyses of
+    TLS 1.3, 5G, and the EMV (Chip-and-pin) standards, in each case
+    finding attacks and proving strong assurance properties for fixed
+    variants of the protocols. Tamarin's formal analysis supports both
+    falsification and unbounded verification in the symbolic model of
+    cryptography.
+
+# -----------------------------------------------------------------------------
+# Properties for individual spotlights page
+# -----------------------------------------------------------------------------
+# Entries here will be shown in the green box on the right of the screen.
+
+# Jumbotron (optional)
+# The path is relative to /assets/img/jumbotrons/
+title_image:
+
+# Title at the top, inside the title-content-container
+title: Tamarin Prover – A Security Protocol Verification Tool
+
+# Add at least one keyword
+keywords:
+    - Formal Verification
+    - Cryptographic Protocols
+
+# The Helmholtz research field
+hgf_research_field: Information
+
+# At least one responsible centre
+# Please use the full and official name of your centre
+hgf_centers:
+    - CISPA Helmholtz Center for Information Security
+
+# List of other contributing organisations (optional)
+contributing_organisations:
+    - name: "ETH Zurich"
+      link_as: https://inf.ethz.ch/
+    - name: "Université de Lorraine"
+      link_as: https://www.loria.fr/en/
+    - name: "University of Oxford"
+      link_as: https://www.cs.ox.ac.uk/
+
+# List of scientific communities
+scientific_community:
+    - Computer Aided Verification
+    - Computer Security
+    - Communication Security
+    - Privacy
+    - Logic and Computation
+    - Formal methods
+
+# Impact on community (optional, not implemented yet)
+impact_on_community:
+
+# An e-mail address
+contact: cremers@cispa.de
+
+# Platforms (optional)
+# Provide platforms in this format
+#   - type: TYPE
+#     link_as: LINK
+# Valid TYPES are: webpage, telegram, mailing-list, twitter, gitlab, github
+# Mailing lists should be added as "mailto:mailinglist@url.de"
+# More types can be implemented by modifying /_layouts/spotlight.html
+platforms:
+    - type: webpage
+      link_as: https://tamarin-prover.github.io/
+    - type: github
+      link_as: https://github.com/tamarin-prover/tamarin-prover
+
+# The software license, please use an SPDX Identifier (https://spdx.org/licenses/) if possible (optional)
+license: GPL-3.0-only
+
+# Is the software pricey or free? (optional)
+costs: free
+
+# What is this software used for in general (e.g. modelling)? (optional, not implemented yet)
+software_type:
+    -
+
+# The applicaiton type (Desktop, Mobile, Web) (optional, not implemented yet)
+application_type:
+    - Web
+
+# List of programming languages (optional)
+programming_languages:
+    - Haskell
+    - Javascript
+
+# DOI (without URL, just 10.1000/1.0000000 ) (optional)
+doi: 10.3233/JCS-210053
+
+# Funding of the software (optional)
+funding:
+    - shortname: # Abbreviation
+      funding_text: # Short text or sentence, if required by your funding guidelines (optional)
+      link_as: # Link (optional)
+---
+
+# Tamarin prover in a nutshell
+
+The Tamarin prover is a tool for the symbolic modelling and analysis of security protocols. It takes as input a security protocol model, specifying the actions taken by agents running the protocol in different roles (e.g., the protocol initiator, the responder, and the trusted key server), a specification of the adversary, and a specification of the protocol’s desired properties. Tamarin can then be used to automatically construct a proof that, even when arbitrarily many instances of the protocol’s roles are interleaved in parallel, together with the actions of the adversary, the protocol fulfils its specified properties; or produce a counterexample that represents an attack on the property.
+
+<div class="spotlights-text-image">
+<img src="{{ site.directory.images | relative_url}}spotlights/tamarin/attack.png" alt="Visual representation of an attack found on the current protocol model.">
+<span>Visual representation of an attack found on the current protocol model.</span>
+</div>
+
+In practice, the Tamarin tool has proven to be highly successful. It features support for trace and observational equivalence properties, automatic and interactive modes. Tamarin has built-in support for fine-grained models of cryptographic primitives through so-called equational theories, such as the one modelling Diffie-Hellman key exchanges. Tamarin has been applied to numerous protocols from different domains including:
+
+* Advanced key agreement protocols based on Diffie-Hellman exponentiation, such as verifying Naxos with respect to the eCK (extended Canetti Krawczyk) model; see (Schmidt et al. 2012).
+* The Attack Resilient Public Key Infrastructure (ARPKI) (Basin et al. 2014).
+* Transport Layer Security (TLS) (Cremers et al. 2016)
+* and many others
+
+
+