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 \emph{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.
@article{arxiv.2501.17824,
title = {SMT-Boosted Security Types for Low-Level MPC},
author = {Christian Skalka and Joseph P. Near},
journal= {arXiv preprint arXiv:2501.17824},
year = {2025}
}
Comments
arXiv admin note: text overlap with arXiv:2407.16504