Single-party protocol API semantics

Before stepping into concrete security and compilation proofs, we perform yet another refinement to our single-party semantics definition, by instantiating the single-party API semantics with a concrete API that relies on a collection of MPC protocols. Such refinement is done first by importing a valid (i.e., with the correct type correspondence) protocol library

(** Language *)
clone import Language.

(** Protocol library that evaluates language values and secret operators *)
clone import ProtocolLibrary with
  type value_t = public_t,
  type inputs_t = secret_t,
  type outputs_t = secret_t,
  type sop_t = sop_t.

Next, we can define a concrete protocol API that uses the protocols disclosed by the protocol library

clone import ProtocolAPI with
  op ProtocolLibrary.n = n,
  type ProtocolLibrary.partyId_t = partyId_t,
  type ProtocolLibrary.value_t = value_t,
  type ProtocolLibrary.inputs_t = inputs_t,
  type ProtocolLibrary.outputs_t = outputs_t,
  type ProtocolLibrary.msg_data = msg_data,
  type ProtocolLibrary.leakage_t = leakage_t,
  type ProtocolLibrary.sideInfo_t = sideInfo_t,
  type ProtocolLibrary.sop_t = sop_t,
  op ProtocolLibrary.sop_spec = sop_spec,
  op ProtocolLibrary.prot_declass = prot_declass,
  op ProtocolLibrary.prot_in = prot_in,
  op ProtocolLibrary.prot_out = prot_out,
  op ProtocolLibrary.prot_sop = prot_sop,
  op ProtocolLibrary.sim_declass = sim_declass,
  op ProtocolLibrary.sim_in = sim_in,
  op ProtocolLibrary.sim_out = sim_out,
  op ProtocolLibrary.sim_sop = sim_sop.

And, finally, we instantiate the single-party API semantics with the protocol API.

clone import SinglePartyAPISemantics with
  theory Language <- Language,
  type API.public_t = public_t,
  type API.inputs_t = inputs_t,
  type API.outputs_t = outputs_t,
  type API.svar_t = svar_t,
  type API.sop_t = sop_t,
  type API.sideInfo_t = sideInfo_t,
  type API.apiCall_data = apiCall_data,
  type API.apiRes_data = apiRes_data,
  type API.apiCallRes = apiCallRes,
  op API.apiCall = ProtocolAPI.apiCall,
  op API.apiRes = ProtocolAPI.apiRes.

Interestingly, although we are using underspecified MPC protocols to define the protocol API, we can still provide a concrete semantics module that evaluates a program by resorting on the protocol API to perform secure operations over confidential data, as shown bellow. In order to perform local computations over non-secret data, the semantics module uses the stepL operator given as part of the single-party API semantics.

module SPSemantics (API : API_t) = {

  var st : configuration_t

  proc init(P : L) : unit = {
    st <- initial_configuration P;
    API.init();
  }
  proc step() : sideInfo_t option = {
    ...
    lst <- sigma st;
    r <- None;
    cst <- callSt lst;

    if (cst = None) {
      newst <- stepL (progSt lst) (envSt lst) (resSt lst);
      if (newst <> None) { st <- upd_sigma (oget newst) st; }
    }
    else {
      match (oget cst) with
      | Call_declass a => { vsio <@ API.declass(a);
                             if (vsio <> None) {
                               (v, si) <- oget vsio;
                               st <- upd_SigmaAPI (Some v) st;
                               r <- Some si; } }
      | Call_in a => ...
      | Call_out a => ...
      | Call_sop sop a pargs sargs => ...
      end;
    }
    return r;
  }
  proc setInput(x: inputs_t): bool = {
    var r <- false;
    if (ib st = None) { r <- true; st <- upd_ib (Some x) st; }
    return r;
  }
  proc getOutput(): outputs_t option = {
    var r: outputs_t option;
    r <- ob st;
    if (r <> None) { st <- upd_ob None st; }
    return r;
  }
}.