diff --git a/_spotlights/tamarin.md b/_spotlights/tamarin.md
new file mode 100644
index 0000000000000000000000000000000000000000..9097761d95e17a97427e0d3c6ab071eff9a17068
--- /dev/null
+++ b/_spotlights/tamarin.md
@@ -0,0 +1,145 @@
+---
+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
+
+
+
diff --git a/assets/img/spotlights/tamarin/attack.png b/assets/img/spotlights/tamarin/attack.png
new file mode 100644
index 0000000000000000000000000000000000000000..91a24d52a583e101cad848ef60010b8b2a901da1
Binary files /dev/null and b/assets/img/spotlights/tamarin/attack.png differ
diff --git a/assets/img/spotlights/tamarin/tamarin.png b/assets/img/spotlights/tamarin/tamarin.png
new file mode 100644
index 0000000000000000000000000000000000000000..b6987ad0fdbcdb95735b5a5137a6edfcdfc472ad
Binary files /dev/null and b/assets/img/spotlights/tamarin/tamarin.png differ