Secure Synthesis of Distributed Cryptographic Applications (Technical Report)

TL;DR

This work tackles the challenge of securely synthesizing distributed cryptographic applications from centralized specifications through secure program partitioning. It develops a simulation-based security proof that spans multiple cryptographic mechanisms, arbitrary corruption, and asynchronous scheduling, unifying information-flow control, choreographic programming, and sequentialization. The pipeline from source program to choreography to endpoint-projected distributed program to cryptographic instantiation is formalized, with a threat model and a structured proof plan that establishes correctness through protocol synthesis and projection, plus a sketch of cryptographic instantiation via $SUC$/$UC$. The results provide a principled basis for end-to-end secure composition of cryptographic protocols and robust hyperproperty preservation, enabling modular security reasoning in practical systems.

Abstract

Developing secure distributed systems is difficult, and even harder when advanced cryptography must be used to achieve security goals. Following prior work, we advocate using secure program partitioning to synthesize cryptographic applications: instead of implementing a system of communicating processes, the programmer implements a centralized, sequential program, which is automatically compiled into a secure distributed version that uses cryptography. While this approach is promising, formal results for the security of such compilers are limited in scope. In particular, no security proof yet simultaneously addresses subtleties essential for robust, efficient applications: multiple cryptographic mechanisms, malicious corruption, and asynchronous communication. In this work, we develop a compiler security proof that handles these subtleties. Our proof relies on a novel unification of simulation-based security, information-flow control, choreographic programming, and sequentialization techniques for concurrent programs. While our proof targets hybrid protocols, which abstract cryptographic mechanisms as idealized functionalities, our approach offers a clear path toward leveraging Universal Composability to obtain end-to-end, modular security results with fully instantiated cryptographic mechanisms. Finally, following prior observations about simulation-based security, we prove that our result guarantees robust hyperproperty preservation, an important criterion for compiler correctness that preserves all source-level security properties in target programs.

Figures (3)

• Figure 1: Overview of compilation and the correctness proof. Left-to-right arrows are compilation steps; $\ge$ are proof steps. Term $w$ is a choreography, $\llbracket \cdot \rrbracket$ is endpoint projection, $\operatorname{src}(\cdot)$ is the inverse of protocol synthesis, and $\llparenthesis \cdot \rrparenthesis$ models corruption. Dashed components represent proof sketches.
• Figure 2: Compiling the Millionaires' Problem
• Figure 3: Syntax of messages and actions.