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.
28 lines
796 B
TeX
28 lines
796 B
TeX
\section{Tamarin vs.\ ProVerif}
|
|
|
|
|
|
ProVerif is another automated protocol verifier. Key differences:
|
|
|
|
\begin{table}[H]
|
|
\centering
|
|
\small
|
|
\begin{tabular}{@{}lll@{}}
|
|
\toprule
|
|
& \textbf{Tamarin} & \textbf{ProVerif} \\
|
|
\midrule
|
|
State & Stateful (multiset rewriting) & Stateless (Horn clauses) \\
|
|
Sessions & Exact, unbounded & Over-approximation \\
|
|
False positives & None & Possible \\
|
|
Automation & Semi-automatic & Fully automatic \\
|
|
Speed & Slower & Faster \\
|
|
Expressiveness & Higher & Lower \\
|
|
\bottomrule
|
|
\end{tabular}
|
|
\caption{Tamarin vs.\ ProVerif comparison.}
|
|
\end{table}
|
|
|
|
Use ProVerif for a quick first check. Use Tamarin for the definitive proof, especially
|
|
for stateful protocols like MPC signing where session state matters.
|
|
|
|
%% ============================================================
|