Karim Eldefrawy

Cryptography, Cybersecurity, Privacy

Co-founder and CTO at Confidencial.io
2017-2021: SRI
2011-2016: HRL Laboratories
2006-2010: PhD@UC Irvine

Scientific curiosity

Scientific knowledge map · Paper #51

A High-Assurance Evaluator for Machine-Checked Secure Multiparty Computation

Karim Eldefrawy and Vitor Pereira

2019 · 26th ACM Conference on Computer and Communications Security (CCS)

  • Theory
  • Applied
  • protocol
  • scheme

Research question

What does the paper try to establish?

Can multiparty and proactive secure-computation protocols against active adversaries be specified and proved in a proof assistant, then turned into executable code while keeping the security argument modular and the performance usable?

Central answer

What is the proposed answer?

The paper builds reusable EasyCrypt abstractions for secret sharing and MPC, proves real/ideal security and sequential-composition lemmas, instantiates them with Shamir/Pedersen, BGW-style arithmetic, refresh/recover, and gradual secret sharing, and extracts OCaml through a new EasyCrypt-to-Why3 toolchain. Microbenchmarks show feasibility while exposing an explicit trusted base of unverified arithmetic, randomness, decoder, and translation components.

Full paper abstract

Abstract

Secure Multiparty Computation (MPC) enables a group of n distrusting parties to jointly compute a function using private inputs. MPC guarantees correctness of computation and confidentiality of inputs if no more than a threshold t of the parties are corrupted. Proactive MPC (PMPC) addresses the stronger threat model of a mobile adversary that controls a changing set of parties (but only up to t at any instant), and may eventually corrupt all n parties over a long time. This paper takes a first stab at developing high-assurance implementations of (P)MPC. We formalize in EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, several abstract and reusable variations of secret sharing and of (P)MPC protocols building on them. Using those, we prove a series of abstract theorems for the proactive setting. We implement and perform computer-checked security proofs of concrete instantiations of the required (abstract) protocols in EasyCrypt. We also develop a new tool-chain to extract high-assurance executable implementations of protocols formalized and verified in EasyCrypt. Our tool-chain uses Why3 as an intermediate tool, and enables us to extract executable code from our (P)MPC formalizations. We conduct an evaluation of the extracted executables by comparing their performance to performance of manually implemented versions using Python-based Charm framework for prototyping cryptographic schemes. We argue that the small overhead of our high-assurance executables is a reasonable price to pay for the increased confidence about their correctness and security.

Provenance: Transcribed from the checked-in full-text PDF; only typography, discretionary hyphenation, and line-break artifacts were normalized.

Evidence profile

Six dimensions, kept separate

The chart summarizes documented evidence and process. It is not a correctness probability, confidence score, or ranking, and no composite score is calculated.

The visual spider chart requires JavaScript. The complete values and rationales follow in text.

LowMediumHighN/A = not assessed

A smaller value means less documented support for that dimension, not that the paper is false or unimportant.

Epistemic evidence High

The full version supplies machine-checked definitions, reductions, composition lemmas, concrete instantiations, extraction examples, explicit TCB limits, and systematic microbenchmarks.

Evaluator security reduction and Theorem 1 Sequential composition lemmas and concrete add/mul/refresh/recover protocols EasyCrypt-to-WhyML translation and Why3-to-OCaml extraction Secret-sharing and MPC microbenchmarks across party/field sizes
Auditability High

A checked-in full author copy with hash/page count, IACR archive, DOI, precise theorem/code/benchmark anchors, and extensive appendices make the represented work inspectable.

Problem, gaps in prior work, contributions, and evaluator overview Public full-version archive identity Official peer-reviewed publication identity
Production provenance Medium

Authors, venue, DOI/ePrint, proof/code scale, toolchain, dependencies, compiler, hardware, and benchmark procedure are documented; roles, revisions, exact repository commits, proof logs, and generated artifact hashes are not.

Official peer-reviewed publication identity EasyCrypt-to-WhyML translation and Why3-to-OCaml extraction Extracted implementations, benchmark environment, and Charm comparison
External scrutiny High

ACM CCS review and machine checking offer strong but different scrutiny surfaces; independent reruns, artifact evaluation status, and public review reports were not located.

Official peer-reviewed publication identity Public full-version archive identity Evaluator security reduction and Theorem 1
Reception Low

OpenAlex reported 7 citations on 2026-07-11; under the finalized rubric, 0 through 8 located citations is Low.

Dated citation-count snapshot
Contribution significance High

The paper crosses from machine-checked multiparty security arguments to extracted executable protocols against active/proactive adversaries and exposes the remaining end-to-end TCB, a substantial methodological contribution despite modest dated citation count.

Problem, gaps in prior work, contributions, and evaluator overview Evaluator security reduction and Theorem 1 Abstracted finite fields, groups, randomness, Reed-Solomon decoder, and translation boundary

Assessment: Ai draft author review pending · 2026-07-11 · rubric 0.2. These dimensions describe documented support and process, not truth, correctness, or a universal ranking. No composite score is calculated.

Top-down and bottom-up view

Hierarchical knowledge map

Collapse a branch for a top-level reading, or follow its source links and child nodes to audit the evidence and boundaries underneath it.

paper

High-assurance MPC evaluator

A machine-checked modular security development and extraction toolchain for executable secret-sharing and proactive MPC components, paired with microbenchmarks and explicit TCB limits.

Problem, gaps in prior work, contributions, and evaluator overview
  4. assumption

    Cryptographic and execution assumptions

    explicit

    Active security uses Pedersen-style commitments and DDH; protocol operation assumes the represented communication model, while concrete execution trusts field/group arithmetic, randomness, and Reed-Solomon implementations.

    Problem, gaps in prior work, contributions, and evaluator overview Abstract sharing, integrity, commitments, VSS, Shamir/Pedersen, and gradual PSS Abstracted finite fields, groups, randomness, Reed-Solomon decoder, and translation boundary
  5. formal framework Abstract reusable EasyCrypt framework machine checked

    Approximately 2K lines define abstract secret-sharing and MPC interfaces; approximately 7K more instantiate them, including about 1K lines of protocol specifications.

    Abstract/concrete proof architecture and code scale
  6. theorem

    Evaluator reduction theorem

    machine checked

    Theorem 1 upper-bounds an adversary's proactive distinguishing advantage against the evaluator by advantages against its VSS and proactive-MPC components, with efficient simulators/reductions.

    Evaluator security reduction and Theorem 1
  7. implementation group Concrete protocol instantiations formalized and extracted

    The development includes Shamir sharing, Pedersen commitments, VSS, additive/batch/gradual sharing, BGW-style addition and multiplication, and refresh/recover protocols.

    Abstract sharing, integrity, commitments, VSS, Shamir/Pedersen, and gradual PSS Sequential composition lemmas and concrete add/mul/refresh/recover protocols Polynomial library, security definitions, and concrete protocol specifications
  8. toolchain

    EasyCrypt → WhyML → OCaml

    implemented with unverified translation

    A syntactic translator maps executable EasyCrypt operators into WhyML, after which Why3's verified extraction generates OCaml; only OCaml is evaluated, though the architecture could target other languages.

    EasyCrypt-to-WhyML translation and Why3-to-OCaml extraction
  9. claim group Principal claims mixed formal and empirical

    The paper claims machine-checked modular security, first-of-kind active BGW verification/extraction, feasible executable performance, and reuse of the abstract framework.

    Problem, gaps in prior work, contributions, and evaluator overview Evaluator security reduction and Theorem 1 Secret-sharing and MPC microbenchmarks across party/field sizes
  10. evidence group

    Evidence stack

    machine checked proofs code and benchmarks

    EasyCrypt definitions/proofs, explicit theorem reductions, code excerpts, a polynomial library, protocol appendices, generated WhyML/OCaml examples, and 100-run median microbenchmarks provide complementary evidence.

    Evaluator security reduction and Theorem 1 Polynomial library, security definitions, and concrete protocol specifications EasyCrypt-to-WhyML translation and Why3-to-OCaml extraction Secret-sharing and MPC microbenchmarks across party/field sizes
  12. limitation group

    Formal and evaluation boundaries

    explicit

    The proof is not UC; BGW active corruption is static rather than adaptive; network/broadcast semantics and low-level libraries are not fully verified; only OCaml and microbenchmarks are evaluated; optimized MPC frameworks are not compared directly.

    Non-UC scope, performance-comparison limits, and future work

Audit trail

Source index

Locators state the depth of the current audit. PDF page numbers, where present, are one-based file pages; metadata-, summary-, and abstract-bounded records explicitly identify their limitations.

  1. Problem, gaps in prior work, contributions, and evaluator overview Abstract and Sections 1-1.3, PDF pages 1-5
  2. Secret sharing, BGW arithmetic, refresh periods, and proactive MPC model Section 2, PDF page 6
  3. Abstract/concrete proof architecture and code scale Sections 3-3.1, PDF pages 6-8
  4. Evaluator security reduction and Theorem 1 Section 3.1, Theorem 1, PDF pages 7-8
  5. Abstract sharing, integrity, commitments, VSS, Shamir/Pedersen, and gradual PSS Section 3.2, PDF pages 8-13
  6. Private/random/proactive functionalities, real/ideal games, and corruption oracles Section 3.3, PDF pages 13-16
  7. Sequential composition lemmas and concrete add/mul/refresh/recover protocols Sections 3.3-3.4, PDF pages 15-18
  8. EasyCrypt-to-WhyML translation and Why3-to-OCaml extraction Section 4 and Figure 19, PDF pages 19-22
  9. Abstracted finite fields, groups, randomness, Reed-Solomon decoder, and translation boundary Sections 1.3, 4, and 5, PDF pages 5, 19-22
  10. Extracted implementations, benchmark environment, and Charm comparison Section 5, PDF pages 22-25
  11. Secret-sharing and MPC microbenchmarks across party/field sizes Section 5 and Tables 2-4, PDF pages 24-26
  12. Non-UC scope, performance-comparison limits, and future work Sections 1.2-1.3, 5, and 7, PDF pages 4-5, 25-27
  13. Polynomial library, security definitions, and concrete protocol specifications Appendices A-D, PDF pages 33-48
  14. Official peer-reviewed publication identity CCS 2019, DOI 10.1145/3319535.3354205
  15. Public full-version archive identity IACR ePrint 2019/922
  16. Dated citation-count snapshot OpenAlex reported 7 citing works on 2026-07-11