mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
abf99d05fc
Restructured from flat .tex/.pdf files into per-paper subdirectories. Added Antje Worring as co-author on all papers. Synced PDFs to pdfs/ for download site.
24 lines
994 B
TeX
24 lines
994 B
TeX
\section{Common Pitfalls}
|
|
|
|
|
|
\subsection{Forgetting to Model the Adversary}
|
|
|
|
If you do not explicitly model what the adversary can learn (via \texttt{Out} facts),
|
|
Tamarin assumes the adversary learns nothing. This makes proofs trivially true and
|
|
useless. Always output public values and consider what the adversary observes.
|
|
|
|
\subsection{Unbounded Sessions}
|
|
|
|
Tamarin verifies properties for an unbounded number of sessions. But this means the
|
|
state space is infinite. If Tamarin does not terminate, try adding \emph{sources lemmas}:
|
|
helper lemmas that constrain where certain facts can originate.
|
|
|
|
\subsection{Equational Theories}
|
|
|
|
Custom equational theories (e.g., for lattice-based cryptography) can make Tamarin's
|
|
unification procedure non-terminating. Stick to built-in theories when possible. For
|
|
post-quantum primitives, model them as uninterpreted functions with explicit
|
|
\texttt{equations} for the decapsulation property.
|
|
|
|
%% ============================================================
|