Paper 2026/884

Formalizing and Strengthening the Security Proof of NTOR

Abstract

We present a machine-checked security proof for the NTOR key exchange protocol, which is used to establish connections in the Tor onion routing system. It was previously studied by Goldberg et al. (DCC 2013) and the protocol ladder project, however there is no full proof including forward secrecy in the computational model. Our proof is formalized in EasyCrypt, adding to the still small set of cryptographic protocols verified using EasyCrypt. A key contribution is a systematic treatment of halting reductions involving failure events expressed as global properties of the execution. In the course of this work, we also contributed improvements to the EasyCrypt framework itself. We prove NTOR secure in a model for unilaterally authenticated key exchange (UAKE) similar to the maximum exposure model by Fiedler et al. (Crypto 2025). It captures forward secrecy concretely, and is intentionally close to established bilaterally authenticated key exchange models (such as eCK) while being simple to formalize. By examining more carefully how identities and public keys are used in key exchange protocols, we obtain simpler formal arguments and introduce several variants of the UAKE security model, connected by general reductions that, in the case of NTOR, are also verified in EasyCrypt. This allows us to carry out the main proof in a simpler setting and then derive the desired security guarantee for NTOR via these reductions.