mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
f4ee7a0525
Bylines, paper authorship, correspondence addresses and the founder blurb under each post named an individual. They name the organisation that published the work instead: the brand on posts and pages, the research byline on papers, and research@ in place of a personal address. Both are what these repositories already used elsewhere — nothing new was coined. Co-authors are untouched. Where a paper named someone else alongside, they stay named; only the one byline changed. Bibliography entries, running heads, PDF metadata and affiliations move with it, so a citation still resolves to whoever the cited paper names. Sample and fixture data uses the placeholder name these tests already use elsewhere, so no assertion changed meaning.
90 lines
2.8 KiB
TeX
90 lines
2.8 KiB
TeX
\documentclass[11pt,a4paper]{article}
|
|
\usepackage{../shared/luxcover}
|
|
\usepackage[utf8]{inputenc}
|
|
\usepackage[T1]{fontenc}
|
|
\usepackage{amsmath,amssymb,amsfonts,amsthm}
|
|
\usepackage{graphicx}
|
|
\usepackage{hyperref}
|
|
\usepackage{booktabs}
|
|
\usepackage{listings}
|
|
\input{../shared/lstlang}
|
|
\usepackage{xcolor}
|
|
\usepackage{enumitem}
|
|
\usepackage{float}
|
|
|
|
\newtheorem{theorem}{Theorem}
|
|
\newtheorem{lemma}[theorem]{Lemma}
|
|
\newtheorem{definition}{Definition}
|
|
\newtheorem{remark}{Remark}
|
|
|
|
\lstdefinelanguage{Tamarin}{
|
|
morekeywords={theory,begin,end,rule,lemma,builtins,functions,equations,
|
|
restriction,axiom,In,Out,Fr,K,All,Ex,not,let,in,if,then,else,
|
|
diffie_hellman,symmetric_encryption,asymmetric_encryption,hashing,
|
|
signing,multiset},
|
|
morecomment=[l]{//},
|
|
morecomment=[s]{/*}{*/},
|
|
morestring=[b]",
|
|
sensitive=true,
|
|
}
|
|
|
|
\lstset{
|
|
basicstyle=\small\ttfamily,
|
|
keywordstyle=\color{blue}\bfseries,
|
|
commentstyle=\color{gray},
|
|
stringstyle=\color{red},
|
|
breaklines=true,
|
|
frame=single,
|
|
numbers=left,
|
|
numberstyle=\tiny\color{gray}
|
|
}
|
|
|
|
\hypersetup{
|
|
colorlinks=true,
|
|
linkcolor=blue,
|
|
citecolor=blue,
|
|
urlcolor=blue
|
|
}
|
|
|
|
\title{Security Protocol Verification with Tamarin Prover}
|
|
\author{
|
|
Lux Research \\
|
|
Lux Industries, Inc.\thanks{Corresponding author: [email protected]}\\
|
|
\texttt{[email protected]}
|
|
}
|
|
\date{2025}
|
|
|
|
\begin{document}
|
|
|
|
\luxcoverpage
|
|
|
|
\begin{abstract}
|
|
Tamarin Prover is a tool for the symbolic analysis of security protocols. It can prove
|
|
that a protocol satisfies security properties (authentication, secrecy, forward secrecy)
|
|
for \emph{all} possible adversary strategies, not just those a tester thought to try.
|
|
This paper teaches Tamarin from first principles: the Dolev-Yao adversary model,
|
|
multiset rewriting rules, lemma specification, and proof strategies. We then present
|
|
Tamarin models of two Lux Network protocols: the MPC bridge signing protocol (FROST-BLS
|
|
threshold signatures over a network adversary) and the hybrid post-quantum TLS handshake
|
|
(combining ML-KEM with X25519 for quantum resistance). For each, we verify authentication,
|
|
secrecy, and agreement properties, and we show how Tamarin's attack finding mode uncovered
|
|
a reflection attack in an early version of the MPC protocol. The reader will learn to
|
|
model protocols, specify security properties, run Tamarin, and interpret its output.
|
|
\end{abstract}
|
|
|
|
\tableofcontents
|
|
\newpage
|
|
|
|
%% ============================================================
|
|
|
|
\input{sections/01-what-is-protocol-verification}
|
|
\input{sections/02-tamarin-fundamentals}
|
|
\input{sections/03-modeling-the-mpc-bridge-protocol}
|
|
\input{sections/04-modeling-the-hybrid-pq-handshake}
|
|
\input{sections/05-running-tamarin}
|
|
\input{sections/06-common-pitfalls}
|
|
\input{sections/07-tamarin-vs-proverif}
|
|
\input{sections/99-conclusion}
|
|
|
|
\end{document}
|