Abstract
Subversion-resilient Authenticated key-exchange (AKE) aims to achieve the guarantees of secure AKE even in the presence of an adversary that has tampered with parts of the protocol’s implementation. One way to achieve subversion-resilient AKE is the use of Reverse Firewalls (RFs), an untrusted third-party that can restore security. Recent work highlights the challenges of designing RFs for practical secure channel-establishment. This paper extends existing RF-based subversion-resilient AKE at three levels: security definitions, constructions, and the use of formal verification. First, we introduce a useful relaxation of the notion of security in subversion-resilient AKE with RFs: the goal is no longer to prevent all exfiltration, but rather to restore to the AKE protocol a property lost upon subversion. We focus specifically on authenticating and (key-)securing RFs. We also discuss subversion-resilience against a spectrum of compromises, designing a flexible framework in which protocols are proved secure with respect to adversaries that can tamper with some components of the implementation, but perhaps not others. Our ultimate goal is to achieve post-quantum secure subversion-resilient key-exchange. Far from being trivial, this requires the introduction of a malleable-yet-secure notion of keyencapsulation, which we dub re-randomizable Key Encapsulation Mechanism. We carefully formalize this new primitive and instantiate it first based on a classical Diffie-Hellman KEM and one based on Kyber. Finally, we lay the foundations for the formal verification of RF based protocols, by formally proving our protocol with the CryptoVerif prover, in addition to computational-security proofs in usual Bellare-Rogaway methodology.
