Multi-party semantics

The multi-party semantics class establishes how a program can be collaboratively animated. We define the multi-party semantics assuming that program evaluation is carried out by three computing nodes, each one holding a description of the program in potentially different languages L1, L2 and L3. We restrict the multi-party semantics to only three parties due to tool limitations. Nevertheless, having a three-party set is explanatory enough to demonstrate the concepts we want to explore in this work and the definitions here presented can be easily extended to other party configurations.

Our multi-party semantics formalisation is based on adversarial code, influenced by the UC model. Program evaluation is managed by an environment, that can provide inputs to the program being interpreted and also collect outputs at any time. Furthermore, the environment can request the evaluation of the program in a small-step basis. This evaluation is carried out by an adversary, that, at a high-level, models the inside behaviour of the environment inside the program execution.

The adversary has the possibility of either request some local party execution or a synchronised execution, where all parties, executing at the same time, have the ability to perform distributed protocols that require party interaction.

Finally, the semantics here specified contemplates the possibility of the execution disclosing the communication trace that is left by operations that result from the collaboration of parties.

Semantics interface

The semantics interface discloses 6 procedures:

• init(P) - initialises the evaluation with initial program P

• stepP(id) - locally executes party id.

• stepS - executes the entire set of parties at the same time. This procedure should be used to perform operations that require party synchronisation.

• stepInput(x) - processes the input x provided by the environment

• getOutput - releases output to the environment

module type Semantics = {
  proc init(P1 : L1.L, P2 : L2.L, P3 : L3.L) : unit
  proc stepP(id : partyId_t) : bool
  proc stepS() : sideInfo_t option
  proc setInput(x : secret_t) : bool
  proc getOutput() : secret_t option
}.

We enforce that the only procedure inside the multi-party semantics that is able to generate visible side information is the synchronised stepS method. Local party execution modeled by stepP does not encompass any visible information, as it simply computes some local operation.

Environment interface

The environment semantics interface specifies how the environment interacts with the program evaluation. It discloses 3 procedures:

• stepInput(x) - provides input x to the program semantics

• getOutput - collects output from the program

• activate - activates the adversary so that it can procede with the actual program evaluation.

module type EnvSemInterface = {
  proc setInput(x: secret_t): bool
  proc getOutput(): secret_t option
  proc activate(): sideInfo_t option
}.

The environment has oracle access to the environment semantics interface in order to animate some program via the animate procedure. To represent the output of some program animation, we enrich the formalisation with a special output_event_t type.

module type Environment (ESI: EnvSemInterface) = {
  proc animate(): output_event_t
}.

Adversary interface

The adversary semantics interface specifies how the adversary interacts with the program evaluation. It discloses 2 procedures:

• stepP(id) - locally executes party id

• stepS - performs a synchronised execution of the entire set of parties

module type AdvSemInterface = {
  proc stepP(id: partyId_t): bool
  proc stepS(): sideInfo_t option
}.

The adversary has oracles access to the adversary semantics interface in order to execute one instruction of a program via the step procedure.

module type Adversary (ASI : AdvSemInterface) = {
  proc step() : sideInfo_t option
}.

General evaluation strategy

Armed with the structures previously defined, we can now construct a general evaluation strategy that executes any given program and that ends with the output event that is verified by the environment.

We start by specifying a concrete implementation of the environment semantics oracle that is parameterised by the concrete semantics of the program and by an adversary. This new module EnvironmentSemanticsInterface essentially defines all possible environment operations based on the concrete semantics of the program and based on the evaluation strategies disclosed by the adversary.

module EnvironmentSemanticsInterface (Sem : Semantics) (A : Adversary) = {
  include Sem [-init, setInput, getOutput]
  proc init = Sem.init
  proc setInput (x: secret_t): bool = {
    var r;
    r <@ Sem.setInput(x);
    return r;
  }
  proc getOutput(): secret_t option = {
    var r;
    r <@ Sem.getOutput();
    return r;
  }
  proc activate(): sideInfo_t option = {
    var r;
    r <@ A(Sem).step();
    return r;
  }
}.

Finally, a program can be computed according to the generic procedure displayed bellow. It takes as input 3 programs written in languages L1, L2 and L3, initialises the local semantics module of each party with the respective program and then proceeds with the concrete program execution. It adopts as output the same output given to by the environment.

module Eval(Sem : Semantics, Z : Environment, A : Adversary) = {
  proc eval(P : L) = {
    var b;
    EnvironmentSemanticsInterface(Sem,A).init(P);
    b <@ Z(EnvironmentSemanticsInterface(Sem,A)).animate();
    return (b);
  }
}.