IEEE S\&P (Oakland)

\documentclass[conference,letterpaper,10pt]{IEEEtran}
\IEEEoverridecommandlockouts

\usepackage{cite}
\usepackage{amsmath,amssymb,amsfonts,amsthm}
\usepackage{algorithmic}
\usepackage{graphicx}
\usepackage{textcomp}
\usepackage{xcolor}
\usepackage{booktabs}
\usepackage{url}
\usepackage[hidelinks]{hyperref}
\usepackage{listings}

\lstset{basicstyle=\ttfamily\footnotesize, columns=fullflexible, breaklines=true}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}

\def\BibTeX{{\rm B\kern-.05em{\sc i\kern-.025em b}\kern-.08em
    T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}}

\begin{document}

\title{Formal Verification of Post-Quantum TLS Implementations:\\
       A Scalable Approach}

\author{
\IEEEauthorblockN{First Last}
\IEEEauthorblockA{\textit{University of Example} \\ [email protected]}
\and
\IEEEauthorblockN{Jane Doe}
\IEEEauthorblockA{\textit{Example Research Labs} \\ [email protected]}
\and
\IEEEauthorblockN{John Smith}
\IEEEauthorblockA{\textit{University of Example} \\ [email protected]}
}

\maketitle

\begin{abstract}
Transitioning TLS to post-quantum cryptography risks reintroducing
classes of implementation bugs eliminated over 25 years of refinement.
We present a verification framework that combines symbolic analysis of
protocol state machines with F*-based refinement-type proofs of
cryptographic primitives. Using it, we verified a 38{,}000-LOC
post-quantum TLS stack in 4.2 hours of proof time. During evaluation we
discovered three previously unknown vulnerabilities in production
post-quantum libraries---two nonce-handling bugs and one length-field
issue---which we responsibly disclosed and were assigned CVEs.
\end{abstract}

\begin{IEEEkeywords}
post-quantum cryptography, formal verification, TLS, refinement types
\end{IEEEkeywords}

\section{Introduction}
Post-quantum migration of TLS is well underway, with Kyber and Dilithium
now in standards-track status. Verification tooling has lagged the pace
of deployment: existing verified TLS implementations cover only
classical cryptography.

\paragraph{Contributions.}
\begin{itemize}
\item A verification framework connecting symbolic protocol analysis
  with F*-based refinement-type proofs of cryptographic primitives.
\item Verified implementations of three post-quantum TLS stacks: an
  OpenSSL-PQ, Rustls-PQ, and BoringSSL-PQ fork.
\item Discovery and responsible disclosure of three previously unknown
  vulnerabilities (CVE-2026-XXXX, -YYYY, -ZZZZ).
\item Scalability results: 38k LOC verified in 4.2 proof hours.
\end{itemize}

\section{Background}
Existing verified TLS implementations (miTLS, HACL*) cover classical
cryptography. Post-quantum primitives (Kyber, Dilithium, Falcon) lack
comparable verified implementations, creating risk during the
transition period.

\section{Threat Model}
We assume a classical adversary (no quantum computer) with full network
control. Our guarantees target memory safety, functional correctness
against the specifications, and absence of common logic errors
(nonce reuse, signature malleability).

\section{Framework}
Our framework connects symbolic execution of handshake state machines
(via ProVerif-style analysis) with F*-based refinement types capturing
cryptographic invariants.

\subsection{Key-Exchange Invariants}
We capture correctness of KEM interactions as refinement predicates on
session state. For Kyber, the invariants include (a) proper nonce
domain separation, (b) authenticated labels across rekeys, and
(c) length-prefix well-formedness.

\begin{theorem}
If an implementation $I$ type-checks against our F* specifications,
then $I$ implements the corresponding RFC-specified behavior up to
observational equivalence in the standard model.
\end{theorem}

\section{Case Studies and Disclosures}
We verified three implementations and found three vulnerabilities:
\begin{itemize}
\item \textbf{CVE-2026-XXXX}: nonce reuse in OpenSSL-PQ key derivation
  when two connections share the same ticket.
\item \textbf{CVE-2026-YYYY}: missing length-field validation in
  Rustls-PQ decapsulation, enabling a denial-of-service.
\item \textbf{CVE-2026-ZZZZ}: timing side-channel in BoringSSL-PQ
  signature parsing.
\end{itemize}
All three were disclosed 90 days before submission and patched
before public release.

\section{Implementation and Results}
The framework is 12{,}400 lines of F* plus a 3{,}800-line OCaml harness.
Verification of the three PQ-TLS stacks completed in 2.8h, 4.2h, and
3.5h respectively on a commodity workstation.

\begin{table}[t]
\centering
\small
\begin{tabular}{lcc}
\toprule
Stack & LOC verified & Proof time (h) \\
\midrule
OpenSSL-PQ    & 14{,}200 & 2.8 \\
Rustls-PQ     & 11{,}800 & 4.2 \\
BoringSSL-PQ  & 12{,}000 & 3.5 \\
\bottomrule
\end{tabular}
\caption{Verification scale and cost.}
\end{table}

\section{Related Work}
miTLS, HACL*, EverCrypt, ProVerif, Tamarin.

\section{Conclusion}
Post-quantum TLS deserves the same verification maturity as the
classical variant. Our framework is a practical step toward that goal.

\section*{Ethics Considerations}
All discovered vulnerabilities were responsibly disclosed 90 days prior
to publication. No real user data was accessed during testing.

\section*{Acknowledgments}
We thank the IEEE S\&P reviewers and the security teams at OpenSSL,
Rustls, and BoringSSL for their cooperation during disclosure.

\bibliographystyle{IEEEtran}
\bibliography{refs}

\end{document}