Secure and correct execution of the X3DH protocol through runtime verification

Abstract

The secure implementation of cryptographic protocols is essential for ensuring the confidentiality and integrity of sensitive information. Previous work has been devoted to the static verification of security protocol designs, utilizing techniques such as model checking and formal proof methods. These static verification techniques aim to analyse the design or source code of a system before execution to ensure its correctness and adherence to security properties. However, static verification often relies on implicit assumptions about the correctness of protocol implementations, which may not hold in practice. These assumptions can be particularly challenging for implementations that were not initially developed with formal verification in mind. To address this issue, this project proposes an approach that leverages runtime verifi‐ cation. Verifying runtime implementations is essential in distributed systems since errors which may not be detectable through static analysis can still introduce vulnerabilities into a system which can cause unexpected when running a distributed application on an unreliable network such as one located across multiple sites separated by vast distances or operated on different platform versions/configurations than anticipated during de‐ velopment testing stages. Furthermore, verifying implementations provides additional assurances against intentional attacks aimed specifically at compromising the security features offered by the protocol itself by preventing attackers from introducing subtle bugs directly into critical points within an application’s source code. To demonstrate the effectiveness of this approach, runtime verification is applied to the open‐source implementation python‐x3dh of the X3DH protocol, a decentralized key management system for end‐to‐end encryption. The protocol allows the estab‐ lishment of secure communication sessions between two or more parties without any prior knowledge of each other’s public keys. This makes it an attractive solution for ap‐ plications that need to use end‐to‐end encryption in a distributed environment, such as communications networks and peer‐to‐peer networks like protocols used by online messaging services.