We model and analyze the Signal end-to-end messaging protocol within the UC framework. In particular: - We formulate an ideal functionality that captures end-to-end secure messaging, in a setting with PKI and an untrusted server, against an adversary that has full control over the network and can adaptively and momentarily compromise parties at any time and obtain their entire internal states. In particular our analysis captures the forward secrecy and recovery-of-security properties of Signal and the conditions under which they break. - We model the main components of the Signal architecture (PKI and long-term keys, the backbone continuous-key-exchange or "asymmetric ratchet," epoch-level symmetric ratchets, authenticated encryption) as individual ideal functionalities that are realized and analyzed separately and then composed using the UC and Global-State UC theorems. - We show how the ideal functionalities representing these components can be realized using standard cryptographic primitives under minimal hardness assumptions. Our modeling introduces additional innovations that enable arguing about the security of Signal irrespective of the underlying communication medium, as well as secure composition of dynamically generated modules that share state. These features, together with the basic modularity of the UC framework, will hopefully facilitate the use of both Signal-as-a-whole and its individual components within cryptographic applications. Two other features of our modeling are the treatment of fully adaptive corruptions, and making minimal use of random oracle abstractions. In particular, we show how to realize continuous key exchange in the plain model, while preserving security against adaptive corruptions.
more »
« less
Short Concurrent Covert Authenticated Key Exchange (Short cAKE)
on Ahn, Hopper and Langford introduced the notion of steganographic a.k.a. covert computation, to capture distributed computation where the attackers must not be able to distinguish honest parties from entities emitting random bitstrings. This indistinguishability should hold for the duration of the computation except for what is revealed by the intended outputs of the computed functionality. An important case of covert computation is mutually authenticated key exchange, a.k.a. mutual authentication. Mutual authentication is a fundamental primitive often preceding more complex secure protocols used for distributed computation. However, standard authentication implementations are not covert, which allows a network adversary to target or block parties who engage in authentication. Therefore, mutual authentication is one of the premier use cases of covert computation and has numerous real-world applications, e.g., for enabling authentication over steganographic channels in a network controlled by a discriminatory entity. We improve on the state of the art in covert authentication by presenting a protocol that retains covertness and security under concurrent composition, has minimal message complexity, and reduces protocol bandwidth by an order of magnitude compared to previous constructions. To model the security of our scheme we develop a UC model which captures standard features of secure mutual authentication but extends them to covertness. We prove our construction secure in this UC model. We also provide a proof-of-concept implementation of our scheme.
more »
« less
- Award ID(s):
- 2030575
- PAR ID:
- 10616428
- Publisher / Repository:
- Springer Nature Singapore
- Date Published:
- Page Range / eLocation ID:
- 75 to 109
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
null (Ed.)We present a secure two-factor authentication (TFA) scheme based on the user’s possession of a password and a crypto-capable device. Security is “end-to-end” in the sense that the attacker can attack all parts of the system, including all communication links and any subset of parties (servers, devices, client terminals), can learn users’ passwords, and perform active and passive attacks, online and offline. In all cases the scheme provides the highest attainable security bounds given the set of compromised components. Our solution builds a TFA scheme using any Device-enhanced Password-authenticated Key Exchange (PAKE), defined by Jarecki et al., and any Short Authenticated String (SAS) Message Authentication, defined by Vaudenay. We show an efficient instantiation of this modular construction, which utilizes any password-based client-server authentication method, with or without reliance on public-key infrastructure. The security of the proposed scheme is proven in a formal model that we formulate as an extension of the traditional PAKE model. We also report on a prototype implementation of our schemes, including TLS-based and PKI-free variants, as well as several instantiations of the SAS mechanism, all demonstrating the practicality of our approach. Finally, we present a usability study evaluating the viability of our protocol contrasted with the traditional PIN-based TFA approach in terms of efficiency, potential for errors, user experience, and security perception of the underlying manual process. 1more » « less
-
A protocol for two-party secure function evaluation (2P-SFE) aims to allow the parties to learn the output of function f of their private inputs, while leaking nothing more. In a sense, such a protocol realizes a trusted oracle that computes f and returns the result to both parties. There have been tremendous strides in efficiency over the past ten years, yet 2P-SFE protocols remain impractical for most real-time, online computations, particularly on modestly provisioned devices. Intel's Software Guard Extensions (SGX) provides hardware-protected execution environments, called enclaves, that may be viewed as trusted computation oracles. While SGX provides native CPU speed for secure computation, previous side-channel and micro-architecture attacks have demonstrated how security guarantees of enclaves can be compromised. In this paper, we explore a balanced approach to 2P-SFE on SGX-enabled processors by constructing a protocol for evaluating f relative to a partitioning of f. This approach alleviates the burden of trust on the enclave by allowing the protocol designer to choose which components should be evaluated within the enclave, and which via standard cryptographic techniques. We describe SGX-enabled SFE protocols (modeling the enclave as an oracle), and formalize the strongest-possible notion of 2P-SFE for our setting. We prove our protocol meets this notion when properly realized. We implement the protocol and apply it to two practical problems: privacy-preserving queries to a database, and a version of Dijkstra's algorithm for privacy-preserving navigation. Our evaluation shows that our SGX-enabled SFE scheme enjoys a 38x increase in performance over garbled-circuit-based SFE. Finally, we justify modeling of the enclave as an oracle by implementing protections against known side-channels.more » « less
-
This article presents a novel network protocol that incorporates a quantum photonic channel for symmetric key distribution, a Dilithium signature to replace factor-based public key cryptography for enhanced authentication, security, and privacy. The protocol uses strong hash functions to hash original messages and verify heightened data integrity at the destination. This Quantum good authentication protocol (QGP) provides high-level security provided by the theory of quantum mechanics. QGP also has the advantage of quantum-resistant data protection that prevents current digital computer and future quantum computer attacks. QGP transforms the transmission control protocol/internet protocol (TCP/IP) by adding a quantum layer at the bottom of the Open Systems Interconnection (OSI) model (layer 0) and modifying the top layer (layer 7) with Dilithium signatures, thus improving the security of the original OSI model. In addition, QGP incorporates strong encryption, hardware-based quantum channels, post-quantum signatures, and secure hash algorithms over a platform of decryptors, switches, routers, and network controllers to form a testbed of the next-generation, secure quantum internet. The experiments presented here show that QGP provides secure authentication and improved security and privacy and can be adopted as a new protocol for the next-generation quantum internet.more » « less
-
Mobile tracking has long been a privacy problem, where the geographic data and timestamps gathered by mobile network operators (MNOs) are used to track the locations and movements of mobile subscribers. Additionally, selling the geolocation information of subscribers has become a lucrative business. Many mobile carriers have violated user privacy agreements by selling users’ location history to third parties without user consent, exacerbating privacy issues related to mobile tracking and profiling. This paper presents AAKA, an anonymous authentication and key agreement scheme designed to protect against mobile tracking by honest-but-curious MNOs. AAKA leverages anonymous credentials and introduces a novel mobile authentication protocol that allows legitimate subscribers to access the network anonymously, without revealing their unique (real) IDs. It ensures the integrity of user credentials, preventing forgery, and ensures that connections made by the same user at different times cannot be linked. While the MNO alone cannot identify or profile a user, AAKA enables identification of a user under legal intervention, such as when the MNOs collaborate with an authorized law enforcement agency. Our design is compatible with the latest cellular architecture and SIM standardized by 3GPP, meeting 3GPP’s fundamental security requirements for User Equipment (UE) authentication and key agreement processes. A comprehensive security analysis demonstrates the scheme’s effectiveness. The evaluation shows that the scheme is practical, with a credential presentation generation taking∼ 52 ms on a constrained host device equipped with a standard cellular SIM.more » « less
An official website of the United States government

