-- ---------------------------------------------------
-- constants, types and variables

const
  NumCustomers:  1;
  NumMerchants:  1;
  NumAcquirers:  1;
  NumIntruders:  1;
  NetworkSize:   1;
  MaxKnowledge:  1;

  EVE_INIT: true;

type
  CustomerId: scalarset (NumCustomers);
  MerchantId: scalarset (NumMerchants);
  AcquirerId: scalarset (NumAcquirers);
  IntruderId: scalarset (NumIntruders);

  AgentId: union {CustomerId, MerchantId, AcquirerId, IntruderId};

  MessageType: enum {
    M_Initiate,
    M_Invoice,
    M_Payment,
    M_AuthRequest,
    M_AuthResponse,
    M_Confirm
  };

  Message : record
    source: AgentId;
    dest: AgentId;
    key: AgentId;
    mType: MessageType;
    salt: AgentId;          -- customer
    cid: AgentId;           -- customer
    mid: AgentId;           -- merchant
    nonce: AgentId;         -- merchant
    desc: AgentId;
    encslip: AgentId;       -- customer
    yn: AgentId;            -- acquirer
    sig: AgentId;
  end;

  CustomerStates : enum {
    C_SLEEP,
    C_WAIT,
    C_AUTH,
    C_COMMIT
  };

  Customer : record
    state: CustomerStates;
    merchant: AgentId;
  end;

  MerchantStates : enum {
    M_SLEEP,
    M_WAIT,
    M_AUTH,
    M_COMMIT
  };

  Merchant : record
    state: MerchantStates;
    customer: AgentId;
    acquirer: AgentId;
  end;

  AcquirerStates : enum {
    A_SLEEP
  };

  Acquirer : record
    state: AcquirerStates;
    merchant: AgentId;
  end;

  Intruder : record
    salts: array[AgentId] of boolean;
    descs: array[AgentId] of boolean;
    messages: multiset[MaxKnowledge] of Message;
  end;

var
  net: multiset[NetworkSize] of Message;
  cus: array[CustomerId] of Customer;
  mer: array[MerchantId] of Merchant;
  acq: array[AcquirerId] of Acquirer;
  int: array[IntruderId] of Intruder;


-- ---------------------------------------------------------------------
-- rules

-- Initiate: customer i starts protocol with merchant j
ruleset i: CustomerId do
  ruleset j: AgentId do
    rule "Initiate"
      cus[i].state = C_SLEEP &
      ismember(j,MerchantId) &
      multisetcount (l:net, true) < NetworkSize
    ==>
    var
      outM: Message;
    begin
      undefine outM;
      outM.source := i;
      outM.dest := j;
      outM.mType := M_Initiate;
      outM.salt := i;
      outM.cid := i;
      multisetadd (outM,net);
      cus[i].state := C_WAIT;
      cus[i].merchant := j;
    end;
  end;
end;

-- Invoice: merchant i sends to customer
ruleset i: MerchantId do
  choose j: net do
    rule "Invoice"
      mer[i].state = M_SLEEP &
      net[j].dest = i
    ==>
    var
      outM: Message;
      inM: Message;
    begin
      inM := net[j];
      multisetremove (j,net);
      if inM.mType=M_Initiate then
        undefine outM;
        outM.source := i;
        outM.dest := inM.source;
        outM.mType := M_Invoice;
        outM.mid := i;
        outM.nonce := i;
        mer[i].customer := inM.source;
        mer[i].state := M_WAIT;
        multisetadd (outM,net);
      end;
    end;
  end;
end;

-- Payment: customer i sends EncSlip to merchant
ruleset i: CustomerId do
  choose j: net do
    rule "Payment"
      cus[i].state = C_WAIT &
      net[j].dest = i
    ==>
    var
      outM: Message;
      inM: Message;
    begin
      inM := net[j];
      multisetremove (j,net);
      if inM.mType=M_Invoice then
        undefine outM;
        outM.source := i;
        outM.dest := cus[i].merchant;
        outM.mType := M_Payment;
        outM.encslip := i;
        cus[i].state := C_AUTH;
        multisetadd(outM,net);
      end;
    end;
  end;
end;

-- AuthRequest: merchant i sends salt, encslip to acquirer
ruleset i: MerchantId do
  choose j: net do
    rule "AuthRequest"
      mer[i].state = M_WAIT &
      cus[mer[i].customer].state = C_AUTH &
      net[j].dest = i
    ==>
    var
      outM: Message;
      inM: Message;
    begin
      inM := net[j];
      multisetremove (j,net);
      if inM.mType=M_Payment then
        undefine outM;
        outM.source := i;
        outM.dest := mer[i].acquirer;
        outM.mType := M_AuthRequest;
        outM.encslip := mer[i].customer;
        outM.salt := mer[i].customer;
        outM.desc := mer[i].customer;
        mer[i].state := M_AUTH;
        multisetadd(outM,net);
      end;
    end
  end;
end;

-- Auth-Response: acquirer i sends sig to merchant
ruleset i: AcquirerId do
  choose j: net do
    rule 90 "AuthResponse"
      net[j].dest = i
    ==>
    var
      outM: Message;
      inM: Message;
    begin
      inM := net[j];
      multisetremove (j,net);
      if inM.mType=M_AuthRequest then
        undefine outM;
        outM.source := i;
        outM.dest := inM.source;
        outM.mType := M_AuthResponse;
        outM.sig := i;
        multisetadd(outM,net);
      end;
    end;
  end;
end;

-- Confirm: merchant i sends sig to customer
ruleset i: MerchantId do
  choose j: net do
    rule "Confirm"
      mer[i].state = M_AUTH &
      net[j].dest = i
    ==>
    var
      outM: Message;
      inM: Message;
    begin
      inM := net[j];
      multisetremove (j,net);
      if inM.mType=M_AuthResponse then
        undefine outM;
        outM.source := i;
        outM.dest := mer[i].customer;
        outM.mType := M_Confirm;
        outM.sig := inM.source;
        mer[i].state := M_COMMIT;
        multisetadd(outM,net);
      end;
    end;
  end;
end;

-- End: customer receives Confirm
ruleset i: CustomerId do
  choose j: net do
    rule "End"
      cus[i].state = C_AUTH &
      mer[cus[i].merchant].state = M_COMMIT &
      net[j].dest = i
    ==>
    var
      inM: Message;
    begin
      inM := net[j];
      multisetremove (j,net);
      if inM.mType=M_Confirm then
        cus[i].state := C_COMMIT;
      end;
    end;
  end;
end;

-- intruder i intercepts messages
ruleset i: IntruderId do
  choose j: net do
    rule "Interception"
    !ismember (net[j].source, IntruderId)
  ==>
  var
    temp: Message;
    begin
      alias msg: net[j] do
        if msg.mType=M_AuthRequest then
          int[i].descs[msg.desc] := true;
        else
          if msg.mType=M_Initiate & EVE_INIT then
            int[i].salts[msg.salt] := true;
          end;
        end;
      end;
    end;
  end;
end;

-- ------------------------------------------------------------------
-- startstate
startstate
  undefine cus;
  for i: CustomerId do
    cus[i].state := C_SLEEP;
    cus[i].merchant := i;
  end;
  undefine mer;
  for i: MerchantId do
    mer[i].state := M_SLEEP;
    mer[i].customer := i;
  end;
  undefine acq;
  for i: AcquirerId do
    acq[i].state := A_SLEEP;
    for j: MerchantId do
      mer[j].acquirer := i;
    end
  end;
  undefine int;
  for i: IntruderId do
    for j: AgentId do
      int[i].salts[j] := false;
      int[i].descs[j] := false;
    end;
  end;
  undefine net;
end;


-- -------------------------------------------------------------------
-- invariants

-- Intruder never knows desc and salt from same customer
invariant "Intruder does not know DESC"
  forall i: IntruderId do
    forall j: CustomerId do
    !int[i].descs[j] |
    !int[i].salts[j]
  end
end;
