papers/lux-protocol-verification-tamarin/sections/01-what-is-protocol-verification.tex

\section{What Is Protocol Verification}


\subsection{The Problem}

Cryptographic primitives (AES, SHA-256, ECDSA) are well-studied and presumed secure.
But combining secure primitives into a protocol does not automatically produce a secure
protocol. The protocol's \emph{message flow}---who sends what to whom, in what order,
with what checks---introduces new attack surfaces: replay attacks, man-in-the-middle,
reflection attacks, interleaving attacks.

These attacks exploit the protocol logic, not the cryptography. They are extremely hard
to find by code review or testing because they require reasoning about all possible
adversary behaviors, not just one.

\subsection{The Dolev-Yao Model}

Tamarin works in the \emph{Dolev-Yao} adversary model:
\begin{itemize}[nosep]
  \item The adversary controls the network completely: it can intercept, delay, replay,
    and modify any message.
  \item The adversary can perform any cryptographic operation on values it knows (encrypt,
    decrypt with known keys, hash, sign with known keys).
  \item The adversary \emph{cannot} break cryptographic primitives: it cannot decrypt
    without the key, it cannot forge signatures without the private key, it cannot
    invert hash functions.
\end{itemize}

This is a ``perfect cryptography'' model. It separates protocol logic bugs from
cryptographic implementation bugs, allowing each to be analyzed independently.

\subsection{What Tamarin Proves}

Given a protocol model and a security property, Tamarin either:
\begin{enumerate}[nosep]
  \item \textbf{Proves} the property holds for all possible adversary strategies and all
    numbers of protocol sessions (unbounded verification).
  \item \textbf{Finds an attack}: a concrete sequence of adversary actions that violates
    the property.
  \item \textbf{Does not terminate}: the search space is infinite, and Tamarin's heuristics
    fail to converge (rare in practice, common in theory).
\end{enumerate}

%% ============================================================