A model for asynchronous reactive systems and its application to secure message transmission

TLDR

The paper proposes a rigorous model for secure reactive systems in asynchronous networks, enabling abstract specifications and composition, and demonstrates it with a complete specification of Secure Message Transmission that improves on prior work and verifies an implementation. The model adopts the simulatability framework of modern cryptography, accommodates diverse network structures and trust models—including static and adaptive adversaries—and proves security via a general theorem on encryption in reactive multi-user settings that extends Bellare et al.'s result. The model facilitates modular security proofs, bridging rigorous cryptographic techniques with tool-supported formal proofs. Citation: al (2000).

Abstract

We present a rigorous model for secure reactive systems in asynchronous networks with a sound cryptographic semantics, supporting abstract specifications and the composition of secure systems. This enables modular proofs of security, which is essential in bridging the gap between the rigorous proof techniques of cryptography and tool-supported formal proof techniques. The model follows the general simulatability approach of modern cryptography. A variety of network structures and trust models can be described such as static and adaptive adversaries, some examples of this are given. As an example of our specification methodology we provide an abstract and complete specification for Secure Message Transmission, improving on recent results by Lynch (1999), and verify one concrete implementation. Our proof is based on a general theorem on the security of encryption in a reactive multi-user setting, generalizing a recent result by Bellare et. al (2000).