International Association
for Cryptologic Research

<p>Space networking has become an increasing area of development with the advent of commercial satellite networks such as those hosted by Starlink and Kuiper, and increased satellite and space presence by governments around the world. Yet, historically such network designs have not been made public, leading to limited formal cryptographic analysis of the security offered by them. One of the few public protocols used in space networking is the Bundle Protocol, which is secured by Bundle Protocol Security (BPSec), an Internet Engineering Task Force (IETF) standard. We undertake a first analysis of BPSec under its default security context, building a model of the secure channel security goals stated in the IETF standard, and note issues therein with message loss detection. We prove BPSec secure, and also provide a stronger construction, one that supports the Bundle Protocol's functionality goals while also ensuring destination awareness of missing message components.</p>

Current messaging protocols are incapable of detecting active man-in-the-middle threats after a state compromise. Even strongly-secure protocols such as Signal, which offers forward secrecy and post-compromise security, are dependent on the adversary being passive immediately following state compromise, and healing guarantees are lost if the attacker is not. In addition, despite a great deal of research analyzing the confidentiality properties of secure messaging, entity authentication has largely been abstracted away. Modern messaging applications often rely on out-of-band communication to achieve entity authentication, with human users actively engaging with the protocol, verifying and attesting to long-term public keys. This is done primarily to reduce reliance on trusted third parties (by replacing that role with the user), but this implies that an accurate picture such messaging application's security must take this interaction into account. In this presentation, we examine these gaps by formalizing user-mediated entity authentication, introducing a security model for capturing user authentication in real-world ratcheted messaging protocols. We further demonstrate that the Signal application’s user-mediated authentication protocol cannot be proven secure in this strong model and suggest a new solution that allows the detection of an active state-compromising adversary. Our solution – the MoDUSA protocol – achieves active post-compromise entity authentication security, under certain assumptions on the out-of-band communication channel. These results have direct implications for existing and future ratcheted secure messaging applications.