--------------------------------------------------------------------------------
--
--  Murphi Model of the XML-Security
--
--------------------------------------------------------------------------------
--
--  version:      1.0
--
--  written by:   Jun Yoshida
--  date:         March 2004
--  affiliation:  Stanford University (visiting scholar from Hitachi)
--
--------------------------------------------------------------------------------
--
--  only the following four steps of the protocol are modeled:
--
--  A->B: {E1}PKb, {SSKa}PKb
--  B->A: {E2}PKa, {SSKb}PKa
--  A->B: {E3}SSKb
--  B->A: {E4}SSKa
--
--  A: Client, B: Server
--  Ex: XML elements, PKx: public key, SSKx: shared secret key
--
--------------------------------------------------------------------------------



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


--------------------------------------------------------------------------------
const
  NumClients:     1;
  NumServers:     1;
  NumIntruders:   1;
  NetworkSize:    1;
  MaxKeys:        10;
--------------------------------------------------------------------------------
type
  ClientId:       scalarset (NumClients);
  ServerId:       scalarset (NumServers);
  IntruderId:     scalarset (NumIntruders);
  AgentId:        union {ClientId, ServerId, IntruderId};

--------------------------------------------------------------------------------
-- messages

MessageType : enum {       -- different types of messages
  M_PK,                    -- public key based messages
  M_SSK                    -- shared secret key based messages
};

SharedSecretKeyId: 1..MaxKeys;

Message: record
  source:   AgentId;           -- source of message
  dest:     AgentId;           -- intended destination of message
  mType:    MessageType;
  element1: AgentId;           -- encrypted XML elements
  enKey1_1: AgentId;           -- public key for encryption
  enKey1_2: SharedSecretKeyId; -- shared secret key for encryption
  element2: SharedSecretKeyId; -- encrypted shared secret key
  enKey2:   AgentId;           -- public key for encryption
end;

--------------------------------------------------------------------------------
-- client

ClientStatus : enum {
  C_SLEEP,
  C_WAIT_PK_MESSAGE,
  C_WAIT_SSK_MESSAGE,
  C_DONE
};

Client : record
  state:  ClientStatus;
  server: AgentId;           -- server which client wants to contact
  cSSK:   SharedSecretKeyId; -- shared secret key for client
  sSSK:   SharedSecretKeyId; -- shared secret key for server
end;

--------------------------------------------------------------------------------
-- server

ServerStatus : enum {
  S_SLEEP,
  S_COMMIT_PK_MESSAGE,
  S_COMMIT_SSK_MESSAGE
};

Server : record
  state:  ServerStatus;
  client: AgentId;
  cSSK:   SharedSecretKeyId; -- shared secret key for client
  sSSK:   SharedSecretKeyId; -- shared secret key for server
end;

--------------------------------------------------------------------------------
-- intruder
Intruder : record
  elements: array[AgentId] of boolean;       -- known XML elements
  keys: array[SharedSecretKeyId] of boolean; -- known shared secret keys
end;

--------------------------------------------------------------------------------
var                                       -- state variables for
  net: multiset[NetworkSize] of Message;  -- network
  cli: array[ClientId] of Client;         -- clients
  ser: array[ServerId] of Server;         -- servers
  int: array[IntruderId] of Intruder;     -- intruders
  nextKey: SharedSecretKeyId;             -- next shared secret key

--------------------------------------------------------------------------------
-- procedures and functions
--------------------------------------------------------------------------------
-- generate next shared secret key
function GenSharedSecretKey(): SharedSecretKeyId;
var
  r: SharedSecretKeyId;
begin
  if isundefined(nextKey) then
    error "out of shared secret keys";
  end;
  r := nextKey;
  if nextKey = MaxKeys then
    undefine nextKey;
  else
    nextKey := nextKey + 1;
  end;
  return r;
end;

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

--------------------------------------------------------------------------------
-- behavior of clients
--------------------------------------------------------------------------------
-- Client i sends a public key based message to Server j
ruleset i: ClientId do
  ruleset j: ServerId do
    rule "client sends pk based message to server"
      cli[i].state = C_SLEEP &
      multisetcount (l:net, true) < NetworkSize
    ==>
    var
      outM: Message;           -- outgoing message
      cSSK: SharedSecretKeyId; -- shared secret key for client
    begin
      cSSK          := GenSharedSecretKey();
      undefine outM;
      outM.source   := i;
      outM.dest     := j;
      outM.mType    := M_PK;
      outM.element1 := i;
      outM.enKey1_1 := j;
      outM.element2 := cSSK;
      outM.enKey2   := j;
      multisetadd (outM, net);
      cli[i].state  := C_WAIT_PK_MESSAGE;
      cli[i].server := j;
      cli[i].cSSK   := cSSK;
    end;
  end;
end;

-- Client i sends a shared secret key based message to Server
ruleset i: ClientId do
  choose j: net do
    rule "client sends sk based message to server"
      cli[i].state = C_WAIT_PK_MESSAGE &
      net[j].dest = i
    ==>
    var
      outM: Message;           -- outgoing message
      inM:  Message;           -- incoming message
      sSSK: SharedSecretKeyId; -- shared secret key for Server
    begin
      inM := net[j];
      multisetremove (j, net);
      if inM.mType = M_PK then
        if inM.enKey1_1 = i & inM.enKey2 = i then
          sSSK          := inM.element2;
          undefine outM;
          outM.source   := i;
          outM.dest     := cli[i].server;
          outM.mType    := M_SSK;
          outM.element1 := i;
          outM.enKey1_2 := sSSK;
          multisetadd (outM, net);
          cli[i].state  := C_WAIT_SSK_MESSAGE;
          cli[i].sSSK   := sSSK;
        else
          --error "client received incorrect pk message"
        end;
      end;
    end;
  end;
end;

-- Client i receives a shared secret key based message from Server
ruleset i: ClientId do
  choose j: net do
    rule "client receives ssk based message from server"
      cli[i].state = C_WAIT_SSK_MESSAGE &
      net[j].dest = i
    ==>
    var
      inM:  Message;   -- incoming message
    begin
      inM := net[j];
      multisetremove (j, net);
      if inM.mType = M_SSK then
        if inM.enKey1_2 = cli[i].cSSK then
          cli[i].state := C_DONE;
        else
          --error "client received incorrect ssk message"
        end;
      end;
    end;
  end;
end;

--------------------------------------------------------------------------------
-- behavior of servers
--------------------------------------------------------------------------------
-- Server i receives a public key based message from Client
ruleset i: ServerId do
  choose j: net do
    rule "server receives pk based message from client"
      ser[i].state = S_SLEEP &
      net[j].dest = i
    ==>
    var
      outM: Message;           -- outgoing message
      inM:  Message;           -- incoming message
      cSSK: SharedSecretKeyId; -- shared secret key for Client
      sSSK: SharedSecretKeyId; -- shared secret key for Server
    begin
      inM := net[j];
      multisetremove (j, net);
      if inM.mType = M_PK then
        if inM.enKey1_1 = i & inM.enKey2 = i then
          sSSK          := GenSharedSecretKey();
          cSSK          := inM.element2;
          undefine outM;
          outM.source   := i;
          outM.dest     := inM.source;
          outM.mType    := M_PK;
          outM.element1 := i;
          outM.enKey1_1 := inM.source;
          outM.element2 := sSSK;
          outM.enKey2   := inM.source;
          multisetadd (outM,net);
          ser[i].state  := S_COMMIT_PK_MESSAGE;
          ser[i].client := inM.source;
          ser[i].cSSK   := cSSK;
          ser[i].sSSK   := sSSK;
        else
          --error "server received incorrect pk message"
       end;
      end;
    end;
  end;
end;

-- Server i receives a shared secret key based message from Client
ruleset i: ServerId do
  choose j: net do
    rule "server receives sk based message from client"
      ser[i].state = S_COMMIT_PK_MESSAGE &
      net[j].dest = i
    ==>
    var
      outM: Message; -- outgoing message
      inM:  Message; -- incoming message
    begin
      inM := net[j];
      multisetremove (j, net);
      if inM.mType = M_SSK then
        if inM.enKey1_2 = ser[i].sSSK then
          undefine outM;
          outM.source   := i;
          outM.dest     := inM.source;
          outM.mType    := M_SSK;
          outM.element1 := i;
          outM.enKey1_2 := ser[i].cSSK;
          multisetadd (outM, net);
          ser[i].state  := S_COMMIT_SSK_MESSAGE;
        else
          --error "server received incorrect ssk message"
        end;
      end;
    end;
  end;
end;

--------------------------------------------------------------------------------
-- behavior of intruders
--------------------------------------------------------------------------------
-- intruder i overhears and/or intercepts messages
ruleset i: IntruderId do
  choose j: net do
    ruleset intercept : boolean do
      rule "intruder overhears/intercepts"
        !ismember(net[j].source, IntruderId) -- not for intruder's message
      ==>
      begin
        alias msg: net[j] do -- message to overhear/intercept
          -- learn public key based messages
          if msg.mType = M_PK then
            if msg.enKey1_1 = i then
              int[i].elements[msg.element1] := true;
            end;
            if msg.enKey2 = i then
              int[i].keys[msg.element2] := true;
            end;
          end;
          -- learn shared secret key based messages
          if msg.mType = M_SSK & int[i].keys[msg.enKey1_2] = true then
            int[i].elements[msg.element1] := true;
          end;
        end;
      end;
    end;
  end;
end;

-- generate key, change message
ruleset i: IntruderId do
  choose j: net do
    ruleset intercept : boolean do
      rule "intruder overhears/intercepts and alter ssk"
        !ismember(net[j].source, IntruderId) -- not for intruder's message
      ==>
      var
        iSSK: SharedSecretKeyId; -- shared secret key for intruder
      begin
        alias msg: net[j] do -- message to overhear/intercept
          if msg.mType = M_PK then
            iSSK              := GenSharedSecretKey();
            msg.element2      := iSSK;
            int[i].keys[iSSK] := true;
          end;
        end;
      end;
    end;
  end;
end;

--------------------------------------------------------------------------------
-- startstate
--------------------------------------------------------------------------------

startstate
  -- initialize clients
  undefine cli;
  for i: ClientId do
    cli[i].state := C_SLEEP;
  end;

  -- initialize servers
  undefine ser;
  for i: ServerId do
    ser[i].state := S_SLEEP;
  end;

  -- initialize intruders
  undefine int;
  for i: IntruderId do
    for j: AgentId do
      int[i].elements[j] := false;
    end;
    for j: SharedSecretKeyId do
      int[i].keys[j] := false;
    end;
  end;

  -- initialize network
  undefine net;

  -- initialize shared secret key generator
  nextKey := 1;
end;

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

invariant "client secrecy"
  forall i: ClientId do
    ismember(cli[i].server, ServerId)
    ->
    forall j: IntruderId do
      int[j].elements[i] = false
    end
  end;

invariant "server secrecy"
  forall i: ServerId do
    ismember(ser[i].client, ClientId)
    ->
    forall j: IntruderId do
      int[j].elements[i] = false
    end
  end;
