SMT-Boosted Security Types for Low-Level MPC

2025/01/29 by Skalka, Christian, Near, Joseph P. · 1 citation
#Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Programming Languages (cs.PL)

paper · doi:10.48550/arxiv.2501.17824

Abstract

Secure Multi-Party Computation (MPC) is an important enabling technology for data privacy in modern distributed applications. We develop a new type theory to automatically enforce correctness,confidentiality, and integrity properties of protocols written in the Prelude/Overture language framework. Judgements in the type theory are predicated on SMT verifications in a theory of finite fields, which supports precise and efficient analysis. Our approach is automated, compositional, scalable, and generalizes to arbitrary prime fields for data and key sizes.

Cited by

• Parallel SMT Solving via Dynamic Partitioning, Core-Guided Pruning, and Backbone Detection

Related

• Language-Based Security for Low-Level MPC
• Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head
• DT-SIM: Property-Based Testing for MPC Security
• How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation
• Modes of Operation Suitable for Computing on Encrypted Data