The rise of 5G and IoT has shifted secure communication from centralized and homogeneous to a landscape of heterogeneous mobile devices constantly travelling between myriad networks. In such environments, it is desirable for devices to securely extend their connection from one network to another, often referred to as a handover. In this work we introduce the first cryptographic formalisation of secure handover schemes. We leverage our formalisation to propose path privacy, a novel security property for handovers that has hitherto remained unexplored. We further develop a syntax for secure handovers, and identify security properties appropriate for secure handover schemes. Finally, we introduce a generic handover scheme that captures all the strong notions of security we have identified, combining our novel path privacy concept with other security properties characteristic to existing handover schemes, demonstrating the robustness and versatility of our framework.

The Secure Shell (SSH) protocol is one of the first security protocols on the Internet to upgrade itself to resist attacks against future quantum computers, with the default adoption of the “quantum (otherwise, classically)” secure hybrid key exchange in OpenSSH from April 2022. However, there is a lack of a comprehensive security analysis of this quantum-resistant version of SSH in the literature: related works either focus on the hybrid key exchange in isolation and do not consider security of the overall protocol, or analyze the protocol in security models which are not appropriate for SSH, especially in the “post-quantum” setting. In this paper, we remedy the state of affairs by providing a thorough post-quantum cryptographic analysis of SSH. We follow a “top-down” approach wherein we first prove security of SSH in a more appropriate model, namely, our post-quantum extension of the so-called authenticated and confidential channel establishment (ACCE) protocol security model; our extension which captures “harvest now, decrypt later” attacks could be of independent interest. Then we establish the cryptographic properties of SSH's underlying primitives, as concretely instantiated in practice, based on our protocol-level ACCE security analysis: for example, we prove relevant cryptographic properties of “Streamlined NTRU Prime”, a key encapsulation mechanism (KEM) which is used in recent versions of OpenSSH and TinySSH, in the quantum random oracle model, and address open problems related to its analysis in the literature. Notably, our ACCE security analysis of post-quantum SSH relies on the weaker notion of IND-CPA security of the ephemeral KEMs used in the hybrid key exchange. This is in contrast to prior works which rely on the stronger assumption of IND-CCA secure ephemeral KEMs. Hence we conclude the paper with a discussion on potentially replacing IND-CCA secure KEMs in current post-quantum implementations of SSH with simpler and faster IND-CPA secure counterparts, and also provide the corresponding benchmarks.

With the proliferation of 5G networks, it is essential to prioritise robust security and seamless compatibility with existing infrastructure. The Authentication and Key Agreement (AKA) and Handover (HO) protocols are crucial in securing communication links and maintaining user privacy in 5G networks. While 5G-AKA represents a significant improvement over its predecessors, it still cannot achieve some important security features, such as perfect forward security (PFS) and forward privacy (PFP), leaving data confidentiality and user privacy susceptible to compromise. Moreover, linkability vulnerabilities in the 5G-AKA pose additional privacy concerns, particularly in the face of active adversaries seeking to compromise user anonymity. To enhance the security and privacy of 5G protocols (5G-AKA and 5G-HO) , we aim to achieve PFS and PFP while aligning with 5G's symmetric-key foundations. In this article, we introduce Pretty Good User Privacy (PGUP), a novel symmetric-based scheme aimed at addressing security and privacy vulnerabilities in the current 5G-AKA and HO protocols. In this article, we introduce a new variant of Puncturable Key Wrapping (i.e., PKW+), which allows us to ensure PFS and PFP while maintaining resilience against DoS (desynchronization) attacks in our proposed protocols. We demonstrate that our proposed scheme is resilient against all the essential security threats by performing a comprehensive formal security analysis. We also conduct relevant experiments to show the cost-effectiveness of the proposed scheme.

The rapid digitization of aviation communication and its dependent critical operations demand secure protocols that address domain-specific security requirements within the unique functional constraints of the aviation industry. These secure protocols must provide sufficient security against current and possible future attackers, given the inherent nature of the aviation community, that is highly complex and averse to frequent upgrades as well as its high safety and cost considerations. In this work we propose a pair of quantum-secure hybrid key exchange protocols ($\mathsf {PQAG}\hbox{-}\mathsf {KEM}$and$\mathsf {PQAG}\hbox{-}\mathsf {SIG}$) to secure communication between aircrafts in-flight and ground stations.$\mathsf {PQAG}\hbox{-}\mathsf {KEM}$leverages post-quantum and classical Key Encapsulation Mechanisms ($\mathsf {KEM}$s) to ensure the hybrid security of the protocol against classical as well as future quantum adversaries.$\mathsf {PQAG}\hbox{-}\mathsf {SIG}$, alternatively, uses quantum-safe digital signatures to achieve authentication security. We provide an implementation of both$\mathsf {PQAG}\hbox{-}\mathsf {KEM}$and$\mathsf {PQAG}\hbox{-}\mathsf {SIG}$, and compare favourably with current state-of-the-art secure avionic protocols. Finally, we provide a formal analysis of our new$\mathsf {PQAG}$protocols in a strong hybrid key exchange framework.

Introducing Small Cell Networks (SCN) has significantly improved wireless link quality, spectrum efficiency and network capacity, which has been viewed as one of the key technologies in the fifth-generation (5G) mobile network. However, this technology increases the frequency of handover (HO) procedures caused by the dense deployment of cells in the network with reduced cell coverage, bringing new security and privacy issues. The current 5G-AKA and HO protocols are vulnerable to security weaknesses, such as the lack of forward secrecy and identity confusion attacks. The high HO frequency of HOs might magnify these security and privacy concerns in the 5G mobile network. This work addresses these issues by proposing a secure privacy-preserving universal HO scheme (UniHand) for SCNs in 5G mobile communication. UniHand can achieve mutual authentication, strong anonymity, perfect forward secrecy, keyescrow-free and key compromise impersonation (KCI) resilience. To the best of our knowledge, this is the first scheme to achieve secure, privacy-preserving universal HO with KCI resilience for roaming users in 5G environment. We demonstrate that our proposed scheme is resilient against all the essential security threats by performing a comprehensive formal security analysis and conducting relevant experiments to show the cost-effectiveness of the proposed scheme.

Focusing on its cryptographic core, we provide the first formal description of the Matrix secure group messaging protocol. Observing that no existing secure messaging model in the literature captures the relationships (and shared state) between users, their devices and the groups they are a part of, we introduce the Device-Oriented Group Messaging model to capture these key characteristics of the Matrix protocol. Utilising our new formalism, we determine that Matrix achieves the basic security notions of confidentiality and authentication, provided it introduces authenticated group membership. On the other hand, while the state sharing functionality in Matrix conflicts with advanced security notions in the literature – forward and post-compromise security – it enables features such as history sharing and account recovery, provoking broader questions about how such security notions should be conceptualised.

We report several practically-exploitable cryptographic vulnerabilities in the Matrix standard for federated real-time communication and its flagship client and prototype implementation, Element. These, together, invalidate the confidentiality and authentication guarantees claimed by Matrix against a malicious server. This is despite Matrix’ cryptographic routines being constructed from well-known and -studied cryptographic building blocks. The vulnerabilities we exploit differ in their nature (insecure by design, protocol confusion, lack of domain separation, implementation bugs) and are distributed broadly across the different subprotocols and libraries that make up the cryptographic core of Matrix and Element. Together, these vulnerabilities highlight the need for a systematic and formal analysis of the cryptography in the Matrix standard.

The 5G mobile communication network provides seamless communication between users and service providers and promises to achieve several stringent requirements, such as seamless mobility and massive connectivity. Although 5G can offer numerous benefits, security and privacy issues still need to be addressed. For example, the inclusion of small cell networks (SCN) into 5G brings the network closer to the connected users, providing a better quality of services (QoS), resulting in a significant increase in the number of Handover procedures (HO), which will affect the security, latency and efficiency of the network. It is then crucial to design a scheme that supports seamless handovers through a secure authentication process. With this aim, in this article, we propose a secure region-based handover scheme that supports seamless connectivity for SCNs in 5G. Our proposed scheme is based on asymmetric-key-based authenticated key exchange and handover protocols that preserve user privacy and network security while providing a seamless region-based handover mechanism and effective membership revocation management. In this context, we introduce three privacy-preserving protocols, i.e., an initial authentication protocol, an intra-region handover protocol and an inter-region handover protocol, for dealing with three communication scenarios. To the best of our knowledge, this is thefirstpaper to consider the privacy and security in both the intra-region and inter-region handover scenarios in 5G communication with effective membership revocation management support. Detailed security and performance analysis of our proposed scheme is presented to show that it is resilient against many security threats, is cost-effective and provides an efficient solution for 5G-enabled mobile communication.

We introduce PQNoise, a post-quantum variant of the Noise framework. We demonstrate that it is possible to replace the Diffie-Hellman key-exchanges in Noise with KEMs in a secure way. A challenge is the inability to combine key pairs of KEMs, which can be resolved by certain forms of randomness-hardening for which we introduce a formal abstraction. We provide a generic recipe to turn classical Noise patterns into PQNoise patterns. We prove that the resulting PQNoise patterns achieve confidentiality and authenticity in the fACCE model. Moreover we show that for those classical Noise-patterns that have been conjectured or proven secure in the fACCE model our matching PQNoise patterns eventually achieve the same security. Our security proof is generic and applies to any valid PQNoise pattern. This is made possible by another abstraction, called a hash-object, which hides the exact workings of how keying material is processed in an abstract stateful object that outputs pseudorandom keys under different corruption patterns. We also show that the hash chains used in Noise are a secure hash-object. Finally, we demonstrate the practicality of PQNoise delivering benchmarks for several base patterns.

Modern messaging applications often rely on out-of-band communication to achieve entity authentication, with human users 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. Despite a great deal of research focusing on analyzing the confidentiality aspect of secure messaging, the entity authenticity aspect of it, which relies on the user mediation, has been largely assumed away. Consequently, while many existing protocols provide some confidentiality guarantees after a compromise, such as post-compromise security (PCS), authenticity guarantees are generally lost, especially against an active attacker. This leads to potential man-in-the-middle (MitM) attacks. In this work, we address this gap by proposing a model to formally capture user-mediated entity authentication, as used by realworld protocols, that can be composed with any ratcheted key exchange. Our threat model captures active post-compromise entity authentication security. We demonstrate that the Signal application's user-mediated authentication protocol cannot be proven secure in this model and suggest a straightforward fix for Signal that allows the detection of an active adversary. Our results have direct implications for other existing and future ratcheted secure messaging applications.

Abstract We analyze the handshake protocol of the Transport Layer Security (TLS) protocol, version 1.3. We address both the full TLS 1.3 handshake (the one round-trip time mode, with signatures for authentication and (elliptic curve) Diffie–Hellman ephemeral ((EC)DHE) key exchange), and the abbreviated resumption/“PSK” mode which uses a pre-shared key for authentication (with optional (EC)DHE key exchange and zero round-trip time key establishment). Our analysis in the reductionist security framework uses a multi-stage key exchange security model, where each of the many session keys derived in a single TLS 1.3 handshake is tagged with various properties (such as unauthenticated versus unilaterally authenticated versus mutually authenticated, whether it is intended to provide forward security, how it is used in the protocol, and whether the key is protected against replay attacks). We show that these TLS 1.3 handshake protocol modes establish session keys with their desired security properties under standard cryptographic assumptions.

Signal is a new security protocol and accompanying app that provides end-to-end encryption for instant messaging. The core protocol has recently been adopted by WhatsApp, Facebook Messenger, and Google Allo among many others, the first two of these have at least 1 billion active users. Signal includes several uncommon security properties (such as "future secrecy" or "post-compromise security"), enabled by a novel technique called ratcheting in which session keys are updated with every message sent. Despite its importance and novelty, there has been little to no academic analysis of the Signal protocol. We conduct the first security analysis of Signal's key agreement and double ratchet as a multi-stage key exchange protocol. We extract from the implementation a formal description of the abstract protocol, and define a security model which can capture the "ratcheting" key update structure. We then prove the security of Signal's core in our model, demonstrating several standard security properties. We have found no major flaws in the design, and hope that our presentation and results can serve as a starting point for other analyses of this widely adopted protocol.

The Internet Engineering Task Force (IETF) is currently developing the next version of the Transport Layer Security (TLS) protocol, version 1.3. The transparency of this standardization process allows comprehensive cryptographic analysis of the protocols prior to adoption, whereas previous TLS versions have been scrutinized in the cryptographic literature only after standardization. This is even more important as there are two related, yet slightly different, candidates in discussion for TLS 1.3, called draft-ietf-tls-tls13-05 and draft-ietf-tls-tls13-dh-based. We give a cryptographic analysis of the primary ephemeral Diffie-Hellman-based handshake protocol, which authenticates parties and establishes encryption keys, of both TLS 1.3 candidates. We show that both candidate handshakes achieve the main goal of providing secure authenticated key exchange according to an augmented multi-stage version of the Bellare-Rogaway model. Such a multi-stage approach is convenient for analyzing the design of the candidates, as they establish multiple session keys during the exchange.

The Secure Shell (SSH) protocol is widely used to provide secure remote access to servers, making it among the most important security protocols on the Internet. We show that the signed-Diffie--Hellman SSH ciphersuites of the SSH protocol are secure: each is a secure authenticated and confidential channel establishment (ACCE) protocol, the same security definition now used to describe the security of Transport Layer Security (TLS) ciphersuites. While the ACCE definition suffices to describe the security of individual ciphersuites, it does not cover the case where parties use the same long-term key with many different ciphersuites: it is common in practice for the server to use the same signing key with both finite field and elliptic curve Diffie--Hellman, for example. While TLS is vulnerable to attack in this case, we show that SSH is secure even when the same signing key is used across multiple ciphersuites. We introduce a new generic multi-ciphersuite composition framework to achieve this result in a black-box way.