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.
82 lines
2.9 KiB
TeX
82 lines
2.9 KiB
TeX
\section{Tamarin Fundamentals}
|
|
|
|
|
|
\subsection{Multiset Rewriting Rules}
|
|
|
|
Tamarin models protocols as sets of \emph{multiset rewriting rules}. Each rule has:
|
|
\begin{itemize}[nosep]
|
|
\item \textbf{Premises}: facts that must exist (consumed from the state).
|
|
\item \textbf{Actions}: labels recorded in the trace (for specifying properties).
|
|
\item \textbf{Conclusions}: facts produced (added to the state).
|
|
\end{itemize}
|
|
|
|
\begin{lstlisting}[language=Tamarin,caption={A multiset rewriting rule}]
|
|
rule Generate_Key:
|
|
[ Fr(~sk) ] // Premise: fresh random value
|
|
--[ Generated(~sk) ]-> // Action: record in trace
|
|
[ !SecretKey($A, ~sk), // Conclusion: persistent fact
|
|
Out(pk(~sk)) ] // Conclusion: adversary learns public key
|
|
\end{lstlisting}
|
|
|
|
\begin{itemize}[nosep]
|
|
\item \texttt{Fr(\~{}sk)}: a fresh (random) value. The \texttt{\~{}} prefix means ``fresh.''
|
|
\item \texttt{\$A}: a public name (adversary knows it). The \texttt{\$} prefix means ``public.''
|
|
\item \texttt{!SecretKey}: a persistent fact (can be consumed multiple times).
|
|
\item \texttt{Out(pk(\~{}sk))}: sends \texttt{pk(\~{}sk)} to the network (adversary).
|
|
\end{itemize}
|
|
|
|
\subsection{Built-in Cryptographic Functions}
|
|
|
|
Tamarin provides built-in support for common cryptographic operations:
|
|
|
|
\begin{lstlisting}[language=Tamarin,caption={Tamarin builtins}]
|
|
theory MyProtocol
|
|
begin
|
|
|
|
builtins: hashing, signing, asymmetric-encryption,
|
|
diffie-hellman, symmetric-encryption
|
|
|
|
// hashing: h(x) -- one-way function
|
|
// signing: sign(m, sk), verify(sign(m, sk), m, pk(sk)) = true
|
|
// asymmetric-encryption: aenc(m, pk(sk)), adec(aenc(m, pk(sk)), sk) = m
|
|
// diffie-hellman: g^x, (g^x)^y = (g^y)^x
|
|
// symmetric-encryption: senc(m, k), sdec(senc(m, k), k) = m
|
|
|
|
end
|
|
\end{lstlisting}
|
|
|
|
\subsection{Specifying Security Properties}
|
|
|
|
Properties are specified as \emph{lemmas} in first-order temporal logic over the trace:
|
|
|
|
\begin{lstlisting}[language=Tamarin,caption={Security property specification}]
|
|
// Secrecy: the adversary never learns the session key
|
|
lemma session_key_secrecy:
|
|
"All A B k #i.
|
|
SessionKey(A, B, k) @i
|
|
==> not (Ex #j. K(k) @j)"
|
|
|
|
// Authentication: if B thinks it talked to A,
|
|
// then A actually ran the protocol
|
|
lemma authentication:
|
|
"All A B k #i.
|
|
Commit(B, A, k) @i
|
|
==> (Ex #j. Running(A, B, k) @j & j < i)"
|
|
|
|
// Injective agreement: one-to-one correspondence
|
|
lemma injective_agreement:
|
|
"All A B k #i.
|
|
Commit(B, A, k) @i
|
|
==> (Ex #j. Running(A, B, k) @j & j < i
|
|
& not (Ex B2 #i2. Commit(B2, A, k) @i2 & not (#i = #i2)))"
|
|
\end{lstlisting}
|
|
|
|
\begin{itemize}[nosep]
|
|
\item \texttt{@i} binds a timepoint to the trace.
|
|
\item \texttt{K(k)} means the adversary knows \texttt{k}.
|
|
\item \texttt{Commit} and \texttt{Running} are action labels placed in protocol rules.
|
|
\item \texttt{j < i} means timepoint \texttt{j} occurs before \texttt{i}.
|
|
\end{itemize}
|
|
|
|
%% ============================================================
|