index.html

---
title: Home
layout: titlepage
category: home
---

<h1>The Tamarin Prover</h1>

<p>
    Tamarin has been successfully used to analyze and support the development of modern security protocols [<a
        href="https://hal.science/hal-03586826v1/document" class="pdf">PDF</a>, <a
        href="https://ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/publications/pub2017/siglog-tamarin.pdf" class="pdf">PDF</a>],
    including TLS 1.3 [<a href="https://tls13tamarin.github.io/TLS13Tamarin/docs/tls13tamarin-draft21.pdf" class="pdf">PDF</a>, <a
        href="https://cispa.saarland/group/cremers/downloads/papers/CHSV2016-TLS13.pdf" class="pdf">PDF</a>], 5G‑AKA [<a
        href="https://arxiv.org/pdf/1806.10360" class="pdf">PDF</a>, <a
        href="https://cispa.saarland/group/cremers/downloads/papers/CrDe2018-5G.pdf" class="pdf">PDF</a>], Noise [<a
        href="https://cispa.saarland/group/cremers/downloads/papers/Noise-Usenix2020.pdf" class="pdf">PDF</a>], EMV (Chip-and-pin)
    [<a href="https://arxiv.org/pdf/2006.08249.pdf" class="pdf">PDF</a>], and Apple iMessage [<a
        href="https://security.apple.com/blog/imessage-pq3/" class="external" target="_blank">Apple blog</a>, <a
        href="https://www.usenix.org/system/files/usenixsecurity25-linker.pdf" class="pdf">PDF</a>].</p>

<!-- <p>
    {% assign post = site.posts.first %}
    <time class="dt-published" datetime="{{ post.date | date_to_xmlschema }}" itemprop="datePublished">
        {%- assign date_format = site.minima.date_format | default: "%b %-d, %Y" -%}
        {{ post.date | date: date_format }}
        {%- if post.updated_date -%}
        &nbsp// Updated {{ post.updated_date | date: date_format }}
        {%- endif -%}
    </time>:
    <a href="{{ post.url }}">{{ post.title }}</a>
</p> -->

<div class="feature-box">
    <div class="feature-text ">
        <h3>Extensive graphical user interface</h3>
        <p>Automatically find attacks or proofs. Attack graphs show exactly how a property can be violated.</p>
    </div>
    <div class="feature-image ">
        <img src="/assets/images/tamarin-attack.png" width="100%">
    </div>
</div>
<div class="feature-box">
    <div class="feature-text ">
        <h3>Interactive proof construction or attack finding</h3>
        <p>Construct partial proofs, or guide proof/attack search manually. For complex protocols, users can inspect
            partial proofs and write auxiliary lemmas.
        </p>
    </div>
    <div class="feature-image ">
        <img src="/assets/images/tamarin-proof.png" width="100%">
    </div>
</div>
<div class="feature-box">
    <div class="feature-text ">
        <h3>Command-line interface</h3>
        <p>Perform protocol analysis in batch mode using the commandline.</p>
    </div>
    <div class="feature-image ">
        <img src="/assets/images/commandline.png" width="100%">
    </div>
</div>
<div class="feature-box">
    <div class="feature-text ">
        <h3>Model protocol state machines</h3>
        <p>Tamarin's core modeling mechanism uses <a
                href="https://tamarin-prover.com/manual/master/book/005_protocol-specification-rules.html"
                target="manual">multiset rewrite rules</a>. Alternatively, specify protocols using <a
                href="https://tamarin-prover.com/manual/master/book/006_protocol-specification-processes.html"
                target="manual">a process calculus</a>, which are automatically translated into rewrite rules.</p>
    </div>
    <div class="feature-image ">
        <img src="/assets/images/rules.png" width="100%">
    </div>
</div>
<div class="feature-box">
    <div class="feature-text ">
        <h3>Specify security properties</h3>
        <p>Security properties can be specified using a <a
                href="https://tamarin-prover.com/manual/master/book/007_property-specification.html" target="manual">first-order logic with quantification over timepoints</a>.</p>
    </div>
    <div class="feature-image ">
        <img src="/assets/images/properties.png" width="100%">
    </div>
</div>

<p>Want to learn more? Consult Tamarin's extensive <a href="/documentation.html">documentation</a>.</p>