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
End-to-End Secure Mobile Group Messaging with Conversation Integrity and Deniability
In this paper, we describe Mobile CoWPI, a deployable, end-to-end secure mobile group messaging application with proofs of security. Mobile CoWPI allows dynamic groups of users to participate in, join, and leave private, authenticated conversations without requiring the participants to be simultaneously online or maintain reliable network connectivity. We identify the limitations of mobile messaging and how they affect conversational integrity and deniability. We define strong models of these security properties, prove that Mobile CoWPI satisfies these properties, and argue that no protocol that satisfies these properties can be more scalable than Mobile CoWPI. We also describe an implementation of Mobile CoWPI and show through experiments that it is suitable for use in real-world messaging conditions.
more »
« less
- Award ID(s):
- 1814753
- PAR ID:
- 10348529
- Date Published:
- Journal Name:
- Proceedings of the 18th ACM Workshop on Privacy in the Electronic Society
- Volume:
- 2019
- Page Range / eLocation ID:
- 55 to 73
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Web-based applications are attractive due to their portability. To leverage that, many mobile applications are hybrid, incorporating a web component that implements most of their functionality. While solutions for enforcing security exist for both mobile and web applications, enforcing and reasoning about the security of their combinations is difficult. We argue for a combination of static and dynamic analysis for assurance of end-to-end confidentiality in hybrid apps. We show how information flows in hybrid Android applications can be secured through use of SPARTA, a static analyzer for Android/Java, and JEST, a dynamic monitor for JavaScript, connected by a compatibility layer that translates policies and value representations. This paper reports on our preliminary investigation using a case study.more » « less
-
As 5G networks are gradually rolled out worldwide, it is important to ensure that their network infrastructures are resilient against malicious attacks. This work presents VET5G, a new virtual end-to-end testbed for 5G network security research experiments or training activities such as Capture-The-Flag competitions. The distinguishing features of VET5G include a home-grown 5G core network emulator written in Rust to ensure memory and thread safety, integration of OpenAirInterface’s Radio Access Network emulator and the official Android emulator to achieve full end-to-end 5G network emulation, inclusion of a reference P4 software switch to assist with prototyping of defense mechanisms for 5G data planes, implementation of Python APIs for easy 5G network experimentation, and adoption of JupyterHub to support multi-user experimentation. In our experiments we demonstrate how to use VET5G for two attack scenarios in 5G networks as well as its performance when it is used in a 5G hacking project for a Mobile Systems Security course.more » « less
-
Existing End-to-End secure messaging applications trust a single service provider to deliver messages in a consistent order to a consistent group of conversation members. We propose a protocol that removes this single point of failure by using multiple service providers, enforcing conversation integrity as long as one service provider out of N behave honestly. However, this approach could potentially increase the number of entities that learn the metadata for a conversation. In this work we discuss the challenges and provide a protocol that limits the metadata leakage to that of existing messaging applications while still providing strong conversation integrity.more » « less
-
IoT (Internet of Things) devices such as sensors have been actively used in 'fogs' to provide critical data during e.g., disaster response scenarios or in-home healthcare. Since IoT devices typically operate in resource-constrained computing environments at the network-edge, data transfer performance to the cloud as well as end-to-end security have to be robust and customizable. In this paper, we present the design and implementation of a middleware featuring "intermittent" and "flexible" end-to-end security for cloud-fog communications. Intermittent security copes with unreliable network connections, and flexibility is achieved through security configurations that are tailored to application needs. Our experiment results show how our middleware that leverages static pre-shared keys forms a promising solution for delivering light-weight, fast and resource-aware security for a variety of IoT-based applications.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1145/3338498.3358644
