2017/11/17 by Aseem Rastogi, Rastogi, Aseem, Nikhil Swamy +3
Computer Science · #Cryptography and Data Security #FOS: Computer and information sciences #Logic, programming, and type systems #Programming Languages (cs.PL) #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.1711.06467
openalex publication_date 2017/11/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Secure multi-party computation (MPC) enables a set of mutually distrusting parties to cooperatively compute, using a cryptographic protocol, a function over their private data. This paper presents Wys*, a new domain-specific language (DSL) for writing mixed-mode MPCs. Wys* is an embedded DSL hosted in F*, a verification-oriented, effectful programming language. Wys* source programs are essentially F* programs written in a custom MPC effect, meaning that the programmers can use F*'s logic to verify the correctness and security properties of their programs. To reason about the distributed runtime semantics of these programs, we formalize a deep embedding of Wys*, also in F*. We mechanize the necessary metatheory to prove that the properties verified for the Wys* source programs carry over to the distributed, multi-party semantics. Finally, we use F*'s extraction to extract an interpreter that we have proved matches this semantics, yielding a partially verified implementation. Wys* is the first DSL to enable formal verification of MPC programs. We have implemented several MPC protocols in Wys*, including private set intersection, joint median, and an MPC card dealing application, and have verified their correctness and security.