A Formal Model for Secure Multiparty Computation. (arXiv:2306.00308v1 [cs.PL])

Although Secure Multiparty Computation (SMC) has seen considerable
development in recent years, its use is challenging, resulting in complex code
which obscures whether the security properties or correctness guarantees hold
in practice. For this reason, several works have investigated the use of formal
methods to provide guarantees for SMC systems. However, these approaches have
been applied mostly to domain specific languages (DSL), neglecting
general-purpose approaches. In this paper, we consider a formal model for an
SMC system for annotated C …

code complex code computation correctness development practice secure multiparty computation security systems