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.
61 lines
1.7 KiB
TeX
61 lines
1.7 KiB
TeX
\section{Running Tamarin}
|
|
|
|
|
|
\subsection{Installation}
|
|
|
|
\begin{lstlisting}[language=bash,caption={Installing Tamarin}]
|
|
# macOS
|
|
brew install tamarin-prover
|
|
|
|
# From source (Haskell Stack)
|
|
git clone https://github.com/tamarin-prover/tamarin-prover.git
|
|
cd tamarin-prover
|
|
stack install
|
|
\end{lstlisting}
|
|
|
|
\subsection{Running Proofs}
|
|
|
|
\begin{lstlisting}[language=bash,caption={Running Tamarin}]
|
|
# Prove all lemmas
|
|
tamarin-prover --prove FROST_BLS.spthy
|
|
|
|
# Interactive mode (web UI for exploring proof trees)
|
|
tamarin-prover interactive FROST_BLS.spthy
|
|
# Then open http://localhost:3001 in a browser
|
|
|
|
# Prove specific lemma
|
|
tamarin-prover --prove=unforgeability FROST_BLS.spthy
|
|
\end{lstlisting}
|
|
|
|
\subsection{Interpreting Output}
|
|
|
|
Tamarin outputs one of three results for each lemma:
|
|
\begin{itemize}[nosep]
|
|
\item \texttt{verified}: The property holds for all possible adversary strategies.
|
|
\item \texttt{falsified}: An attack was found. Tamarin outputs the attack trace.
|
|
\item \texttt{analysis incomplete}: Tamarin could not determine the result (may require
|
|
manual guidance via proof oracles or lemma ordering).
|
|
\end{itemize}
|
|
|
|
\subsection{Proof Results}
|
|
|
|
\begin{table}[H]
|
|
\centering
|
|
\small
|
|
\begin{tabular}{@{}llrl@{}}
|
|
\toprule
|
|
\textbf{Protocol} & \textbf{Property} & \textbf{Time} & \textbf{Result} \\
|
|
\midrule
|
|
FROST-BLS & Unforgeability & 3.2s & Verified \\
|
|
FROST-BLS & Nonce secrecy & 1.1s & Verified \\
|
|
FROST-BLS & No nonce reuse & 0.4s & Verified \\
|
|
Hybrid handshake & Session secrecy & 2.7s & Verified \\
|
|
Hybrid handshake & Forward secrecy & 8.4s & Verified \\
|
|
Hybrid handshake & Hybrid security & 4.1s & Verified \\
|
|
\bottomrule
|
|
\end{tabular}
|
|
\caption{Tamarin proof results for Lux Network protocol models.}
|
|
\end{table}
|
|
|
|
%% ============================================================
|