Multi-party oracle-aided protocols and semi-honest privacy

This module defines the party-structured syntax and execution semantics of synchronous m-party protocols over pairwise private authenticated point-to-point channels with k-ary ideal oracle calls (MultiOracleSpec), together with Goldreich's joint view-and-output definition of perfect semi-honest privacy against static coalitions (PerfectSemiHonestPrivate).

Each party's view (PartyView) is derived from the protocol execution: it records only that party's own input x i, its own private coins r i drawn from proto.sampleCoins i, the messages addressed to i, and the oracle answer parts for slots assigned to i. In Round.Received, message delivery to receiver has type (i = receiver) → Msg and oracle answer delivery has type (s : Fin (spec.arity op)) → (parties s = i) → spec.Answer op s, so parties outside the recipient set receive functions over an empty proof domain and transport under party embeddings is definitional function composition. Each party's output (Protocol.outputOfView) is extracted deterministically from its own PartyView.

Main definitions

• Cslib.Crypto.Protocols.MPC.MultiOracleSpec, Cslib.Crypto.Protocols.MPC.MultiOracleSpec.toOracleSpec, Cslib.Crypto.Protocols.MPC.MultiOracleWorld, Cslib.Crypto.Protocols.MPC.MultiOracleWorld.handler, Cslib.Crypto.Protocols.MPC.noOracleSpec, Cslib.Crypto.Protocols.MPC.noOracleWorld: k-ary ideal oracle specifications and memoryless worlds.
• Cslib.Crypto.Protocols.MPC.Round, Cslib.Crypto.Protocols.MPC.Schedule, Cslib.Crypto.Protocols.MPC.Round.Received, Cslib.Crypto.Protocols.MPC.Schedule.Received, Cslib.Crypto.Protocols.MPC.PartyView: synchronous communication schedules and derived per-party views.
• Cslib.Crypto.Protocols.MPC.Steps, Cslib.Crypto.Protocols.MPC.Protocol, Cslib.Crypto.Protocols.MPC.Protocol.outputOfView, Cslib.Crypto.Protocols.MPC.Steps.mapState, Cslib.Crypto.Protocols.MPC.Steps.append, Cslib.Crypto.Protocols.MPC.Steps.run, Cslib.Crypto.Protocols.MPC.Protocol.run, Cslib.Crypto.Protocols.MPC.Protocol.evalWith, Cslib.Crypto.Protocols.MPC.Protocol.realJoint: local step-by-step party strategies and their real execution semantics.
• Cslib.Crypto.Protocols.MPC.Functionality, Cslib.Crypto.Protocols.MPC.Functionality.ofDeterministic, Cslib.Crypto.Protocols.MPC.CoalitionSimulator, Cslib.Crypto.Protocols.MPC.idealJoint, Cslib.Crypto.Protocols.MPC.PerfectSemiHonestPrivate, Cslib.Crypto.Protocols.MPC.PerfectSemiHonestPrivateProper: ideal joint view-and-output execution and perfect semi-honest privacy.

Main results

• Cslib.Crypto.Protocols.MPC.Schedule.Received.split_append, Cslib.Crypto.Protocols.MPC.Schedule.Received.append_split: splitting and concatenating received transcripts along concatenated schedules.
• Cslib.Crypto.Protocols.MPC.Protocol.evalWith_eq, Cslib.Crypto.Protocols.MPC.Steps.evalWith_done, Cslib.Crypto.Protocols.MPC.Steps.evalWith_message, Cslib.Crypto.Protocols.MPC.Steps.evalWith_oracle: structural evaluation rules for protocols and steps.
• Cslib.Crypto.Protocols.MPC.PerfectSemiHonestPrivate.proper: full-coalition privacy implies proper-coalition privacy.
• Cslib.Crypto.Protocols.MPC.perfectSemiHonestPrivate_of_deterministic: for deterministic functionalities, matching the marginal coalition view distribution (Eq. 7.39, cf. Eqs. 7.7–7.8) together with output correctness on the support yields full joint view-and-output privacy (Eq. 7.40, cf. Eqs. 7.9–7.10).

References

• O. Goldreich, Foundations of Cryptography, Volume 2: Basic Applications, Section 7.2.2.1 (Definition 7.2.1, pp. 620–622), Section 7.5.1.2 (Definition 7.5.1, pp. 696–697), and Section 7.5.2.1 (Definitions 7.5.5–7.5.6, pp. 701–702).

Multi-party oracle specifications and worlds

structure Cslib.Crypto.Protocols.MPC.MultiOracleSpec : Type 1

Specification of k-ary oracle operations (Goldreich Def. 7.5.5, pp. 701–702).

• Op : Type

  The type of oracle operations.

• arity : self.Op → ℕ

  The arity k of each operation.

• Query (op : self.Op) : Fin (self.arity op) → Type

  The query part submitted by slot s : Fin (arity op).

• Answer (op : self.Op) : Fin (self.arity op) → Type

  The answer part returned to slot s : Fin (arity op).

@[reducible, inline]

abbrev Cslib.Crypto.Protocols.MPC.MultiOracleSpec.toOracleSpec (spec : MultiOracleSpec) : OracleSpec ((op : spec.Op) × ((s : Fin (spec.arity op)) → spec.Query op s))

Underlying OracleSpec of a MultiOracleSpec.

@[reducible, inline]

abbrev Cslib.Crypto.Protocols.MPC.MultiOracleWorld (spec : MultiOracleSpec) : Type

A memoryless implementation (world) of spec.

noncomputable def Cslib.Crypto.Protocols.MPC.MultiOracleWorld.handler {spec : MultiOracleSpec} (W : MultiOracleWorld spec) (q : ℕ ⊕ (op : spec.Op) × ((s : Fin (spec.arity op)) → spec.Query op s)) : PMF (probOracleSpec spec.toOracleSpec q)

Combined PMF handler for ProbOracleComp spec.toOracleSpec in a memoryless world W.

def Cslib.Crypto.Protocols.MPC.noOracleSpec : MultiOracleSpec

The empty multi-party oracle specification (plain point-to-point channel model).

def Cslib.Crypto.Protocols.MPC.noOracleWorld : MultiOracleWorld noOracleSpec

The unique world for noOracleSpec.

Synchronous rounds, schedules, and received transcripts

inductive Cslib.Crypto.Protocols.MPC.Round (m : ℕ) (spec : MultiOracleSpec) : Type 1

A single synchronous step in an m-party protocol over pairwise private point-to-point channels and k-ary oracle spec.

• message {m : ℕ} {spec : MultiOracleSpec} (sender receiver : Fin m) (Msg : Type) : Round m spec

  Point-to-point private message of type Msg from sender to receiver.

• oracle {m : ℕ} {spec : MultiOracleSpec} (op : spec.Op) (parties : Fin (spec.arity op) ↪ Fin m) : Round m spec

  Joint k-ary oracle invocation of op by k distinct parties parties.

@[reducible, inline]

abbrev Cslib.Crypto.Protocols.MPC.Schedule (m : ℕ) (spec : MultiOracleSpec) : Type 1

A fixed-schedule m-party protocol shape over spec.

@[reducible]

def Cslib.Crypto.Protocols.MPC.Round.Received {m : ℕ} {spec : MultiOracleSpec} : Round m spec → Fin m → Type

What party i receives in round r, using proof-domain functions so transport under party embeddings is definitional function composition without if-casts.

def Cslib.Crypto.Protocols.MPC.Round.deliverMessage {m : ℕ} {spec : MultiOracleSpec} {sender receiver : Fin m} {Msg : Type} (msg : Msg) (i : Fin m) : (message sender receiver Msg).Received i

Deliver a point-to-point message msg to receiver; parties i ≠ receiver have an empty proof domain i = receiver.

def Cslib.Crypto.Protocols.MPC.Round.deliverOracle {m : ℕ} {spec : MultiOracleSpec} {op : spec.Op} (parties : Fin (spec.arity op) ↪ Fin m) (ans : (s : Fin (spec.arity op)) → spec.Answer op s) (i : Fin m) : (oracle op parties).Received i

Deliver oracle answer parts ans to the participating parties; for slots s with parties s ≠ i, the proof domain parties s = i is empty.

@[simp]

theorem Cslib.Crypto.Protocols.MPC.Round.deliverMessage_apply {m : ℕ} {spec : MultiOracleSpec} {sender receiver i : Fin m} {Msg : Type} (msg : Msg) (h : i = receiver) : deliverMessage msg i h = msg

@[simp]

theorem Cslib.Crypto.Protocols.MPC.Round.deliverOracle_apply {m : ℕ} {spec : MultiOracleSpec} {op : spec.Op} (parties : Fin (spec.arity op) ↪ Fin m) (ans : (s : Fin (spec.arity op)) → spec.Answer op s) (i : Fin m) (s : Fin (spec.arity op)) (h : parties s = i) : deliverOracle parties ans i s h = ans s

theorem Cslib.Crypto.Protocols.MPC.Round.received_message_eq_of_ne {m : ℕ} {spec : MultiOracleSpec} {sender receiver i : Fin m} {Msg : Type} (hne : i ≠ receiver) (f g : (message sender receiver Msg).Received i) : f = g

For a non-recipient i ≠ receiver, any two received-message records are equal.

theorem Cslib.Crypto.Protocols.MPC.Round.received_message_ext {m : ℕ} {spec : MultiOracleSpec} {sender receiver i : Fin m} {Msg : Type} {f g : (message sender receiver Msg).Received i} (h : ∀ (hr : i = receiver), f hr = g hr) : f = g

Two received-message records at i are equal if they agree when i = receiver.

theorem Cslib.Crypto.Protocols.MPC.Round.received_oracle_ext {m : ℕ} {spec : MultiOracleSpec} {op : spec.Op} {parties : Fin (spec.arity op) ↪ Fin m} {i : Fin m} {f g : (oracle op parties).Received i} (h : ∀ (s : Fin (spec.arity op)) (hs : parties s = i), f s hs = g s hs) : f = g

Two received-oracle records at i are equal if they agree on every slot assigned to i.

@[reducible]

def Cslib.Crypto.Protocols.MPC.Schedule.Received {m : ℕ} {spec : MultiOracleSpec} : Schedule m spec → Fin m → Type

The sequence of values received by party i across all rounds of sc.

def Cslib.Crypto.Protocols.MPC.Schedule.Received.append {m : ℕ} {spec : MultiOracleSpec} {sc₁ sc₂ : Schedule m spec} {i : Fin m} : sc₁.Received i → sc₂.Received i → (sc₁ ++ sc₂).Received i

Concatenate received transcripts along sc₁ and sc₂ into a transcript along sc₁ ++ sc₂.

def Cslib.Crypto.Protocols.MPC.Schedule.Received.split {m : ℕ} {spec : MultiOracleSpec} {sc₁ sc₂ : Schedule m spec} {i : Fin m} : (sc₁ ++ sc₂).Received i → sc₁.Received i × sc₂.Received i

Split a received transcript along sc₁ ++ sc₂ into transcripts along sc₁ and sc₂.

@[simp]

theorem Cslib.Crypto.Protocols.MPC.Schedule.Received.split_append {m : ℕ} {spec : MultiOracleSpec} {sc₁ sc₂ : Schedule m spec} {i : Fin m} (r₁ : sc₁.Received i) (r₂ : sc₂.Received i) : (r₁.append r₂).split = (r₁, r₂)

@[simp]

theorem Cslib.Crypto.Protocols.MPC.Schedule.Received.append_split {m : ℕ} {spec : MultiOracleSpec} {sc₁ sc₂ : Schedule m spec} {i : Fin m} (r : (sc₁ ++ sc₂).Received i) : r.split.1.append r.split.2 = r

structure Cslib.Crypto.Protocols.MPC.PartyView {m : ℕ} {spec : MultiOracleSpec} (In Coins : Fin m → Type) (sc : Schedule m spec) (i : Fin m) : Type

Party i's complete view of an execution along schedule sc (Goldreich Def. 7.2.1, p. 620).

• input : In i

  Party i's input.

• coins : Coins i

  Party i's private random coins.

• received : sc.Received i

  Messages and oracle answers received by party i along sc.

theorem Cslib.Crypto.Protocols.MPC.PartyView.ext_iff {m : ℕ} {spec : MultiOracleSpec} {In Coins : Fin m → Type} {sc : Schedule m spec} {i : Fin m} {x y : PartyView In Coins sc i} : x = y ↔ x.input = y.input ∧ x.coins = y.coins ∧ x.received = y.received

theorem Cslib.Crypto.Protocols.MPC.PartyView.ext {m : ℕ} {spec : MultiOracleSpec} {In Coins : Fin m → Type} {sc : Schedule m spec} {i : Fin m} {x y : PartyView In Coins sc i} (input : x.input = y.input) (coins : x.coins = y.coins) (received : x.received = y.received) : x = y

Party-structured protocols and execution semantics

inductive Cslib.Crypto.Protocols.MPC.Steps {m : ℕ} {spec : MultiOracleSpec} : (Fin m → Type) → (Fin m → Type) → Schedule m spec → Type 1

Local step-by-step party computations along schedule sc, with State and Out as indices after the colon so Lean's kernel accepts the varying state type in next.

• done {m : ℕ} {spec : MultiOracleSpec} {State Out : Fin m → Type} (output : (i : Fin m) → State i → Out i) : Steps State Out []

  End of interaction: each party i deterministically computes its output from its local state.

• message {m : ℕ} {spec : MultiOracleSpec} {State Out : Fin m → Type} {sender receiver : Fin m} {Msg : Type} {sc : Schedule m spec} (send : State sender → Msg) (next : Steps (fun (i : Fin m) => State i × (Round.message sender receiver Msg).Received i) Out sc) : Steps State Out (Round.message sender receiver Msg :: sc)

  Point-to-point message round: sender computes Msg from its local state, receiver receives it, and execution continues with each party's state augmented by its Round.Received record.

• oracle {m : ℕ} {spec : MultiOracleSpec} {State Out : Fin m → Type} {op : spec.Op} {parties : Fin (spec.arity op) ↪ Fin m} {sc : Schedule m spec} (query : (s : Fin (spec.arity op)) → State (parties s) → spec.Query op s) (next : Steps (fun (i : Fin m) => State i × (Round.oracle op parties).Received i) Out sc) : Steps State Out (Round.oracle op parties :: sc)

  Joint k-ary oracle round: each participating party parties s computes its query part from its own local state, the oracle returns answer parts, and execution continues with each party's state augmented by its Round.Received record.

structure Cslib.Crypto.Protocols.MPC.Protocol (m : ℕ) (spec : MultiOracleSpec) (sc : Schedule m spec) (In Coins Out : Fin m → Type) : Type 1

An m-party protocol along schedule sc.

• sampleCoins (i : Fin m) : ProbComp (Coins i)

  Independent private coin sampler for each party i.

• steps : Steps (fun (i : Fin m) => In i × Coins i) Out sc

  Interactive step-by-step party computations starting from (input, coins).

def Cslib.Crypto.Protocols.MPC.Steps.outputAt {m : ℕ} {spec : MultiOracleSpec} {State Out : Fin m → Type} {sc : Schedule m spec} (steps : Steps State Out sc) (i : Fin m) (st_i : State i) (recv_i : sc.Received i) : Out i

Extract party i's output from its own current local state st_i and its own remaining received transcript recv_i along sc.

def Cslib.Crypto.Protocols.MPC.Protocol.outputOfView {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins Out : Fin m → Type} (proto : Protocol m spec sc In Coins Out) (i : Fin m) (v : PartyView In Coins sc i) : Out i

Deterministic extraction of party i's output from its complete PartyView.

def Cslib.Crypto.Protocols.MPC.Steps.run {m : ℕ} {spec : MultiOracleSpec} {State Out : Fin m → Type} {sc : Schedule m spec} (steps : Steps State Out sc) (st : (i : Fin m) → State i) : ProbOracleComp spec.toOracleSpec ((i : Fin m) → sc.Received i)

Execute steps in ProbOracleComp spec.toOracleSpec from current local states st, returning each party's received transcript along sc.

def Cslib.Crypto.Protocols.MPC.Protocol.run {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins Out : Fin m → Type} (proto : Protocol m spec sc In Coins Out) (x : (i : Fin m) → In i) : ProbOracleComp spec.toOracleSpec (((i : Fin m) → PartyView In Coins sc i) × ((i : Fin m) → Out i))

Pinned execution of proto on input tuple x in ProbOracleComp spec.toOracleSpec: samples each party's coins independently, runs proto.steps, and sets outputs to fun i => proto.outputOfView i (views i) by definition.

noncomputable def Cslib.Crypto.Protocols.MPC.Steps.evalWith {m : ℕ} {spec : MultiOracleSpec} {State Out : Fin m → Type} {sc : Schedule m spec} (steps : Steps State Out sc) (W : MultiOracleWorld spec) (st : (i : Fin m) → State i) : PMF ((i : Fin m) → sc.Received i)

Evaluate steps.run st against W : MultiOracleWorld spec via OracleComp.evalWith.

@[simp]

theorem Cslib.Crypto.Protocols.MPC.Steps.evalWith_done {m : ℕ} {spec : MultiOracleSpec} {State Out : Fin m → Type} (output : (i : Fin m) → State i → Out i) (W : MultiOracleWorld spec) (st : (i : Fin m) → State i) : (done output).evalWith W st = PMF.pure fun (x : Fin m) => ()

@[simp]

theorem Cslib.Crypto.Protocols.MPC.Steps.evalWith_message {m : ℕ} {spec : MultiOracleSpec} {State Out : Fin m → Type} {sender receiver : Fin m} {Msg : Type} {sc : Schedule m spec} (send : State sender → Msg) (next : Steps (fun (i : Fin m) => State i × (Round.message sender receiver Msg).Received i) Out sc) (W : MultiOracleWorld spec) (st : (i : Fin m) → State i) : (message send next).evalWith W st = PMF.map (fun (r_tail : (i : Fin m) → sc.Received i) (i : Fin m) => (Round.deliverMessage (send (st sender)) i, r_tail i)) (next.evalWith W fun (i : Fin m) => (st i, Round.deliverMessage (send (st sender)) i))

@[simp]

theorem Cslib.Crypto.Protocols.MPC.Steps.evalWith_oracle {m : ℕ} {spec : MultiOracleSpec} {State Out : Fin m → Type} {op : spec.Op} {parties : Fin (spec.arity op) ↪ Fin m} {sc : Schedule m spec} (query : (s : Fin (spec.arity op)) → State (parties s) → spec.Query op s) (next : Steps (fun (i : Fin m) => State i × (Round.oracle op parties).Received i) Out sc) (W : MultiOracleWorld spec) (st : (i : Fin m) → State i) : (oracle query next).evalWith W st = (W op fun (s : Fin (spec.arity op)) => query s (st (parties s))).eval.bind fun (ans : (s : Fin (spec.arity op)) → spec.Answer op s) => PMF.map (fun (r_tail : (i : Fin m) → sc.Received i) (i : Fin m) => (Round.deliverOracle parties ans i, r_tail i)) (next.evalWith W fun (i : Fin m) => (st i, Round.deliverOracle parties ans i))

noncomputable def Cslib.Crypto.Protocols.MPC.Protocol.evalWith {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins Out : Fin m → Type} (proto : Protocol m spec sc In Coins Out) (W : MultiOracleWorld spec) (x : (i : Fin m) → In i) : PMF (((i : Fin m) → PartyView In Coins sc i) × ((i : Fin m) → Out i))

Evaluate proto.run x against W : MultiOracleWorld spec via OracleComp.evalWith.

def Cslib.Crypto.Protocols.MPC.Steps.mapState {m : ℕ} {spec : MultiOracleSpec} {A B Out : Fin m → Type} {sc : Schedule m spec} (f : (i : Fin m) → A i → B i) (steps : Steps B Out sc) : Steps A Out sc

Precompose a step-by-step protocol computation with a local state transformation f.

@[simp]

theorem Cslib.Crypto.Protocols.MPC.Steps.outputAt_mapState {m : ℕ} {spec : MultiOracleSpec} {A B Out : Fin m → Type} {sc : Schedule m spec} (f : (i : Fin m) → A i → B i) (steps : Steps B Out sc) (i : Fin m) (st_i : A i) (recv_i : sc.Received i) : (mapState f steps).outputAt i st_i recv_i = steps.outputAt i (f i st_i) recv_i

@[simp]

theorem Cslib.Crypto.Protocols.MPC.Steps.run_mapState {m : ℕ} {spec : MultiOracleSpec} {A B Out : Fin m → Type} {sc : Schedule m spec} (f : (i : Fin m) → A i → B i) (steps : Steps B Out sc) (st : (i : Fin m) → A i) : (mapState f steps).run st = steps.run fun (i : Fin m) => f i (st i)

@[simp]

theorem Cslib.Crypto.Protocols.MPC.Steps.evalWith_mapState {m : ℕ} {spec : MultiOracleSpec} {A B Out : Fin m → Type} {sc : Schedule m spec} (f : (i : Fin m) → A i → B i) (steps : Steps B Out sc) (W : MultiOracleWorld spec) (st : (i : Fin m) → A i) : (mapState f steps).evalWith W st = steps.evalWith W fun (i : Fin m) => f i (st i)

def Cslib.Crypto.Protocols.MPC.Steps.append {m : ℕ} {spec : MultiOracleSpec} {State Mid Out : Fin m → Type} {sc₁ sc₂ : Schedule m spec} (steps₁ : Steps State Mid sc₁) (steps₂ : Steps Mid Out sc₂) : Steps State Out (sc₁ ++ sc₂)

Sequentially compose steps₁ : Steps State Mid sc₁ (whose .done node computes each party's intermediate state Mid i) with steps₂ : Steps Mid Out sc₂ along sc₁ ++ sc₂.

@[simp]

theorem Cslib.Crypto.Protocols.MPC.Steps.outputAt_append {m : ℕ} {spec : MultiOracleSpec} {State Mid Out : Fin m → Type} {sc₁ sc₂ : Schedule m spec} (steps₁ : Steps State Mid sc₁) (steps₂ : Steps Mid Out sc₂) (i : Fin m) (st_i : State i) (r₁ : sc₁.Received i) (r₂ : sc₂.Received i) : (steps₁.append steps₂).outputAt i st_i (r₁.append r₂) = steps₂.outputAt i (steps₁.outputAt i st_i r₁) r₂

theorem Cslib.Crypto.Protocols.MPC.Steps.run_append {m : ℕ} {spec : MultiOracleSpec} {State Mid Out : Fin m → Type} {sc₁ sc₂ : Schedule m spec} (steps₁ : Steps State Mid sc₁) (steps₂ : Steps Mid Out sc₂) (st : (i : Fin m) → State i) : (steps₁.append steps₂).run st = do let r₁ ← steps₁.run st let r₂ ← steps₂.run fun (i : Fin m) => steps₁.outputAt i (st i) (r₁ i) pure fun (i : Fin m) => (r₁ i).append (r₂ i)

theorem Cslib.Crypto.Protocols.MPC.Steps.evalWith_append {m : ℕ} {spec : MultiOracleSpec} {State Mid Out : Fin m → Type} {sc₁ sc₂ : Schedule m spec} (steps₁ : Steps State Mid sc₁) (steps₂ : Steps Mid Out sc₂) (W : MultiOracleWorld spec) (st : (i : Fin m) → State i) : (steps₁.append steps₂).evalWith W st = (steps₁.evalWith W st).bind fun (r₁ : (i : Fin m) → sc₁.Received i) => PMF.map (fun (r₂ : (i : Fin m) → sc₂.Received i) (i : Fin m) => (r₁ i).append (r₂ i)) (steps₂.evalWith W fun (i : Fin m) => steps₁.outputAt i (st i) (r₁ i))

theorem Cslib.Crypto.Protocols.MPC.Protocol.evalWith_eq {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins Out : Fin m → Type} (proto : Protocol m spec sc In Coins Out) (W : MultiOracleWorld spec) (x : (i : Fin m) → In i) : proto.evalWith W x = (ProbComp.eval (OracleComp.pi proto.sampleCoins)).bind fun (r : (i : Fin m) → Coins i) => PMF.map (fun (recv : (i : Fin m) → sc.Received i) => have views := fun (i : Fin m) => { input := x i, coins := r i, received := recv i }; (views, fun (i : Fin m) => proto.outputOfView i (views i))) (proto.steps.evalWith W fun (i : Fin m) => (x i, r i))

Unfold proto.evalWith W x into independent coin sampling followed by proto.steps.evalWith W.

theorem Cslib.Crypto.Protocols.MPC.Protocol.snd_eq_outputOfView_of_mem_support_evalWith {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins Out : Fin m → Type} {proto : Protocol m spec sc In Coins Out} {W : MultiOracleWorld spec} {x : (i : Fin m) → In i} {res : ((i : Fin m) → PartyView In Coins sc i) × ((i : Fin m) → Out i)} (h : res ∈ (proto.evalWith W x).support) : res.2 = fun (i : Fin m) => proto.outputOfView i (res.1 i)

Every supported outcome of proto.evalWith W x has outputs equal to proto.outputOfView of its views.

noncomputable def Cslib.Crypto.Protocols.MPC.Protocol.realJoint {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins Out : Fin m → Type} (proto : Protocol m spec sc In Coins Out) (W : MultiOracleWorld spec) (I : Finset (Fin m)) (x : (i : Fin m) → In i) : PMF (((i : ↥I) → PartyView In Coins sc ↑i) × ((i : Fin m) → Out i))

Real joint distribution of the coalition I's views and all m parties' outputs when running proto in world W on inputs x (Goldreich Def. 7.5.1, Eq. 7.40, p. 696).

Ideal functionalities, coalition simulators, and semi-honest privacy

@[reducible, inline]

abbrev Cslib.Crypto.Protocols.MPC.Functionality (m : ℕ) (In Out : Fin m → Type) : Type

A general (possibly randomized) m-party functionality mapping an input tuple to a distribution over output tuples.

def Cslib.Crypto.Protocols.MPC.Functionality.ofDeterministic {m : ℕ} {In Out : Fin m → Type} (f : ((i : Fin m) → In i) → (i : Fin m) → Out i) : Functionality m In Out

Lift a deterministic m-party function to a Functionality.

@[reducible, inline]

abbrev Cslib.Crypto.Protocols.MPC.CoalitionSimulator {m : ℕ} {spec : MultiOracleSpec} (sc : Schedule m spec) (In Coins Out : Fin m → Type) (I : Finset (Fin m)) : Type

A simulator for a static coalition I : Finset (Fin m) receives the coalition's inputs (i : I) → In i and the coalition's outputs (i : I) → Out i, and samples simulated views (i : I) → PartyView In Coins sc i.

def Cslib.Crypto.Protocols.MPC.idealJoint {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins Out : Fin m → Type} (f : Functionality m In Out) (I : Finset (Fin m)) (S : CoalitionSimulator sc In Coins Out I) (x : (i : Fin m) → In i) : ProbComp (((i : ↥I) → PartyView In Coins sc ↑i) × ((i : Fin m) → Out i))

Ideal joint view-and-output sampler (Goldreich Def. 7.2.1 Eqs. 7.9–7.10, p. 620; Def. 7.5.1 Eq. 7.40, p. 696): samples the full functionality output y ← f x, feeds the coalition's inputs and outputs to the simulator S, and returns (v, y).

def Cslib.Crypto.Protocols.MPC.PerfectSemiHonestPrivate {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins Out : Fin m → Type} (proto : Protocol m spec sc In Coins Out) (W : MultiOracleWorld spec) (f : Functionality m In Out) (S : (I : Finset (Fin m)) → CoalitionSimulator sc In Coins Out I) : Prop

Perfect semi-honest privacy for all static coalitions I : Finset (Fin m) (Goldreich Def. 7.5.1, Eq. 7.40, p. 696; cf. Def. 7.2.1, Eqs. 7.9–7.10, p. 620).

def Cslib.Crypto.Protocols.MPC.PerfectSemiHonestPrivateProper {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins Out : Fin m → Type} (proto : Protocol m spec sc In Coins Out) (W : MultiOracleWorld spec) (f : Functionality m In Out) (S : (I : Finset (Fin m)) → CoalitionSimulator sc In Coins Out I) : Prop

Perfect semi-honest privacy against all proper static coalitions I ≠ Finset.univ.

theorem Cslib.Crypto.Protocols.MPC.PerfectSemiHonestPrivate.proper {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins Out : Fin m → Type} {proto : Protocol m spec sc In Coins Out} {W : MultiOracleWorld spec} {f : Functionality m In Out} {S : (I : Finset (Fin m)) → CoalitionSimulator sc In Coins Out I} (h : PerfectSemiHonestPrivate proto W f S) : PerfectSemiHonestPrivateProper proto W f S

Full-coalition perfect semi-honest privacy implies proper-coalition privacy.

theorem Cslib.Crypto.Protocols.MPC.perfectSemiHonestPrivate_of_deterministic {m : ℕ} {spec : MultiOracleSpec} {sc : Schedule m spec} {In Coins Out : Fin m → Type} (proto : Protocol m spec sc In Coins Out) (W : MultiOracleWorld spec) (f : ((i : Fin m) → In i) → (i : Fin m) → Out i) (S : (I : Finset (Fin m)) → CoalitionSimulator sc In Coins Out I) (hView : ∀ (I : Finset (Fin m)) (x : (i : Fin m) → In i), (S I (I.restrict x) (I.restrict (f x))).eval = PMF.map (fun (r : ((i : Fin m) → PartyView In Coins sc i) × ((i : Fin m) → Out i)) => I.restrict r.1) (proto.evalWith W x)) (hOut : ∀ (x : (i : Fin m) → In i), ∀ r ∈ (proto.evalWith W x).support, r.2 = f x) : PerfectSemiHonestPrivate proto W (Functionality.ofDeterministic f) S

Bridge lemma (Goldreich Def. 7.5.1, Eqs. 7.39–7.40, p. 696; cf. Def. 7.2.1, Eqs. 7.7–7.10, p. 620, and equivalence remark on p. 621): for a deterministic functionality f, matching the marginal coalition view distribution (Eq. 7.39, cf. Eqs. 7.7–7.8) together with perfect output correctness on the support yields full joint view-and-output privacy (Eq. 7.40, cf. Eqs. 7.9–7.10).