mirror of
https://github.com/lux-apps/papers.git
synced 2026-11-03 05:07:46 +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.
97 lines
3.0 KiB
TeX
97 lines
3.0 KiB
TeX
\section{Modeling the Hybrid PQ Handshake}
|
|
|
|
|
|
Lux Network uses a hybrid post-quantum TLS handshake that combines X25519 (classical
|
|
Diffie-Hellman) with ML-KEM-768 (post-quantum key encapsulation). The hybrid design
|
|
ensures security even if one scheme is broken.
|
|
|
|
\subsection{Protocol Flow}
|
|
|
|
\begin{enumerate}
|
|
\item \textbf{ClientHello}: Client sends $g^x$ (X25519 ephemeral) and $\mathsf{ek}$
|
|
(ML-KEM encapsulation key).
|
|
\item \textbf{ServerHello}: Server computes $g^y$ (X25519 ephemeral), encapsulates
|
|
$(\mathsf{ct}, K_{\text{pq}}) \leftarrow \mathsf{Encaps}(\mathsf{ek})$, and derives
|
|
the session key: $K = \mathsf{KDF}(g^{xy} \| K_{\text{pq}})$.
|
|
\item \textbf{Finished}: Both sides confirm the session key via MAC.
|
|
\end{enumerate}
|
|
|
|
\subsection{Tamarin Model}
|
|
|
|
\begin{lstlisting}[language=Tamarin,caption={Hybrid handshake in Tamarin}]
|
|
theory HybridHandshake
|
|
begin
|
|
|
|
builtins: diffie-hellman, hashing, symmetric-encryption
|
|
|
|
functions: encaps/2, decaps/2, mlkem_pk/1,
|
|
kdf/1
|
|
|
|
equations: decaps(encaps(k, mlkem_pk(sk)), sk) = k
|
|
|
|
// Client Hello
|
|
rule Client_Hello:
|
|
[ Fr(~x), Fr(~ek_seed) ]
|
|
--[ ClientInit($C, $S, ~x) ]->
|
|
[ ClientState($C, $S, ~x, ~ek_seed),
|
|
Out(<'ClientHello', 'g'^~x, mlkem_pk(~ek_seed)>) ]
|
|
|
|
// Server Hello
|
|
rule Server_Hello:
|
|
[ In(<'ClientHello', gx, ek>),
|
|
Fr(~y), Fr(~k_pq) ]
|
|
--[ let ss = kdf(<gx^~y, ~k_pq>) in
|
|
ServerSession($S, $C, ss),
|
|
Running($S, $C, ss) ]->
|
|
[ ServerState($S, $C, ~y, ~k_pq, kdf(<gx^~y, ~k_pq>)),
|
|
Out(<'ServerHello', 'g'^~y, encaps(~k_pq, ek),
|
|
senc('server_finished', kdf(<gx^~y, ~k_pq>))>) ]
|
|
|
|
// Client Finished
|
|
rule Client_Finished:
|
|
[ ClientState($C, $S, ~x, ~ek_seed),
|
|
In(<'ServerHello', gy, ct, server_fin>) ]
|
|
--[ let k_pq = decaps(ct, ~ek_seed) in
|
|
let ss = kdf(<gy^~x, k_pq>) in
|
|
Eq(server_fin, senc('server_finished', ss)),
|
|
ClientSession($C, $S, ss),
|
|
Commit($C, $S, ss) ]->
|
|
[ Out(senc('client_finished', ss)) ]
|
|
|
|
// Equality check
|
|
restriction Equality:
|
|
"All x y #i. Eq(x, y) @i ==> x = y"
|
|
\end{lstlisting}
|
|
|
|
\subsection{Properties Verified}
|
|
|
|
\begin{lstlisting}[language=Tamarin,caption={Hybrid handshake security properties}]
|
|
// Session key secrecy under Dolev-Yao
|
|
lemma session_secrecy:
|
|
"All C S k #i.
|
|
ClientSession(C, S, k) @i
|
|
& not (Ex #c. Corrupt(C) @c)
|
|
& not (Ex #c. Corrupt(S) @c)
|
|
==> not (Ex #j. K(k) @j)"
|
|
|
|
// Forward secrecy: even if long-term keys are later compromised,
|
|
// past session keys remain secret
|
|
lemma forward_secrecy:
|
|
"All C S k #i #c1 #c2.
|
|
ClientSession(C, S, k) @i
|
|
& Corrupt(C) @c1 & Corrupt(S) @c2
|
|
& i < c1 & i < c2
|
|
==> not (Ex #j. K(k) @j)"
|
|
|
|
// Hybrid security: session key is secure if EITHER
|
|
// DH or ML-KEM is secure (not both need to hold)
|
|
lemma hybrid_security:
|
|
"All C S k #i.
|
|
ClientSession(C, S, k) @i
|
|
& not (Ex #c. Corrupt(C) @c)
|
|
& not (Ex #c. Corrupt(S) @c)
|
|
==> not (Ex #j. K(k) @j)"
|
|
\end{lstlisting}
|
|
|
|
%% ============================================================
|