--------------------------------------------------------------------------------
--
--  Murphi Model of the CHAP protocol, between Authenticator A end Peer P
--
--  MICROSOFT CHAP VERSION 2
--
--------------------------------------------------------------------------------
--
--  steps of the protocol modeled:
--
-- M_Connect
--   P -> A: HELLO
--
-- M_Challenge
--   A -> P: session + serverNonce
--
-- M_Response
--   P -> A: session + peerNonce + {H(peerNonce, serverNonce, peerName)}_pwdh
--
-- M_Success | M_Failure
--   A -> P: session + H( H(pwdh), {H(peerNonce, serverNonce, peerName)}_pwdh, H(peerNonce, serverNonce, peerName))
-- + success || failure
--
--   A: authenticator, P: peer
--  We will also use the term "server" for Authenticator, and "client" for peer.
--
--------------------------------------------------------------------------------
-- SIMPLIFICATIONS:
--
-- This model only considers peers' passwords. It might be better to consider
-- "all" passwords (intruders and peers) but we don't see the point, given that
-- the server will only accept passwords from honest peers anyways.
--------------------------------------------------------------------------------


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
const

	NumAuthenticators:    1;    -- number of authenticators
	NumPeers:             1;    -- number of peers
	NumIntruders:         1;    -- number of intruders
	NetworkSize:          1;    -- max. number of outstanding messages in network
  
	-- Protocol modifiers
	CheckServerAuth:       true;  -- if true, make sure that client only enters success with actual servers
	CheckClientAuth:       false; -- if true, make sure that server only enters success with actual clients
  
	AttackerSendsFailure:  false; -- true if attacker sends password_expired to response instead of server's success


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-- Types defined for this MurPHI model.
type
	-- Set of authenticators
	AuthenticatorId:  scalarset (NumAuthenticators);
	-- Set of peers
	PeerId:           scalarset (NumPeers);
	-- Set of intruders
	IntruderId:       scalarset (NumIntruders);
	-- Set of all possible peers
	PeerIntruder: union {PeerId, IntruderId};
	-- Set of all possible authenticators
	AuthenticatorIntruder: union {AuthenticatorId, IntruderId};
	-- Set of all agents
	AgentId:      union {AuthenticatorId, PeerId, IntruderId};

	MessageType : enum {      -- different types of messages
		M_Connect,             -- Peer says hello to authenticator (link begin)
		M_Challenge,           --  {Challenge,Chall_Id, Chall_Val}
		M_Response,            --  {Resp_Id, Resp_Val}
		M_Success,             --  Success, Peer has been authenticated
		M_Failure,             --  Failure, Peer has failed to be authenticated
		M_Failure_Expired,     --  Failure, expired password (only attacker sends this.)
		M_ChangePassword       --  Change password, sent by client
	};
   
	NTResponse: record
		peerNonce      : PeerIntruder;
		serverNonce    : AuthenticatorIntruder;
		password       : PeerIntruder; -- name assumed to be the same (since
											    -- server can check)
	end;

	Session: record
		server:   AuthenticatorIntruder;
		client:   PeerIntruder;
	end;

   Message : record
      fromIntruder   : Boolean;                 -- Whether the intruder sent this message (so it doesn't learn it again)
      mType          : MessageType;             -- type of message
      session        : Session;                 -- the id of peer + authenticator
      serverNonce    : AuthenticatorIntruder;   -- server or peer nonce
      peerNonce      : PeerIntruder;            -- server or peer nonce
      response       : NTResponse               -- The NT Response or the whole authenticator response
   end;

   AuthenticatorStates : enum {
      A_SLEEP,                     -- waiting for link
      A_LINKED,                    -- state after connexion setup or at any given time during connection
      A_WAIT_RESPONSE,             -- waiting for response from peer
      A_FAILURE,                   -- authenticator refuses to authenticate peer
      A_SUCCESS                    -- authenticator accepts to authenticate peer
   };                              --  (thinks responder is authenticated)

   Authenticator: record
      state:     AuthenticatorStates;
      peer: PeerIntruder;               -- agent who links to the authenticator
   end;
   
   PeerStates : enum {
      P_LINK,                      -- peer is going to make a connection
      P_WAIT_CHALLENGE,            -- peer is waiting for the server's challenge
      P_WAIT_OK,                   -- peer has sent response, waiting for server's OK
      P_SUCCESS,                   -- peer received server OK, and server is authenticated
      P_FAILURE,                   -- peer was told to buzz off
      P_BADAUTH                    -- authenticator failed to provide correct credentials
   };

   Peer : record
      state:     PeerStates;
      authenticator: AuthenticatorIntruder;
   end;
   
   PeerArray : array[PeerIntruder] of boolean;
   AuthenticatorArray : array[AuthenticatorIntruder] of boolean;
   SessionArray: array [AuthenticatorIntruder] of PeerArray;
	ResponseArray: array[PeerIntruder] of SessionArray;

   Intruder : record
      passwords      : PeerArray;                  -- known passwords
      serverNonces   : AuthenticatorArray;         -- known client nonces
      peerNonces     : PeerArray;                  -- known passwords
      NTResponses    : ResponseArray;               -- known NTResponses (peerNonce/serverNonce/peer{pass,name})
      AuthResponses  : ResponseArray;              -- known Authenticator responses
      sessions       : SessionArray;              -- known sessions
   end;
    

-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
var                                               -- state variables for:

  net: multiset[NetworkSize] of Message;          --  network
  auth: array[AuthenticatorId] of Authenticator;  --  authenticators
  peer: array[PeerId] of Peer;                    --  peers
  int: array[IntruderId] of Intruder;             --  intruders



------------------------------------------------------------
------------------------------------------------------------
------------------------------------------------------------
------    ___  ______ _____ _   __________  ___  ____ ------
------   / _ )/ __/ // / _ | | / /  _/ __ \/ _ \/ __/ ------
------  / _  / _// _  / __ | |/ // // /_/ / , _/\ \   ------
------ /____/___/_//_/_/ |_|___/___/\____/_/|_/___/   ------
------                                                ------
------------------------------------------------------------
------------------------------------------------------------
------------------------------------------------------------


---------------------------
--   ___                 --
--  / _ \___ ___ _______ --
-- / ___/ -_) -_) __(_-< --
--/_/   \__/\__/_/ /___/ --
--                       --
---------------------------
--PEERS

-- peer p starts protocol with server or intruder s (step 1)
ruleset p: PeerId do
   ruleset s: AuthenticatorIntruder do
      rule "peer sends Hello (step 1)"

         peer[p].state = P_LINK &
         multisetcount (l:net, true) < NetworkSize  -- only send a message if network is not full

      ==>
    
      var
         outM: Message;   -- outgoing message

      begin
         undefine outM;
         outM.mType := M_Connect;
         outM.fromIntruder := false;
         outM.session.client := p;
         outM.session.server := s;
         multisetadd (outM,net);

         peer[p].state         := P_WAIT_CHALLENGE;
         peer[p].authenticator := s;
      end;
   end;
end;

-- peer i reacts to challenge (step 3)
ruleset p: PeerId do
   choose m: net do
      rule "peer reacts to challenge (step 3)"

         peer[p].state = P_WAIT_CHALLENGE &
         net[m].session.client = p &                     -- Message is for us
         net[m].session.server = peer[p].authenticator & -- message comes from the right server
         net[m].mType = M_Challenge &
         net[m].fromIntruder -- to diminish state space, assume all messages are controlled by intruder
      ==>

      var
         outM: Message;   -- outgoing message
         inM:  Message;   -- incoming message

      begin
         inM := net[m];
         multisetremove (m,net);
         undefine outM;
         -- Create response message
         outM.fromIntruder := false;
         outM.session.client := p;
         outM.session.server := peer[p].authenticator;
         outM.mType    := M_Response;  
         outM.peerNonce := p;
         outM.response.serverNonce := inM.serverNonce;
         outM.response.peerNonce := p;
         outM.response.password := p;
               
         -- Peer challenge
         outM.peerNonce := p;
         -- send message
         multisetadd (outM,net);
         -- update state
         peer[p].state := P_WAIT_OK;
      end;
   end;
end;

-- peer receives a success or failure message (step 5)
ruleset p: PeerId do
   choose m: net do
      rule "peer receives success/failure (step 5)"
      
         peer[p].state = P_WAIT_OK &
         net[m].session.client = p &                     -- Message is for us
         net[m].session.server = peer[p].authenticator & -- message comes from the right server
         (net[m].mType = M_Failure | net[m].mType = M_Success | net[m].mType = M_Failure_Expired) &
         net[m].fromIntruder -- to diminish state space, assume all messages are controlled by intruder
      ==>
      
      var
         inM: Message; -- incoming
         outM: Message; -- potential outgoing
      
      begin
         inM := net[m];
         multisetremove(m, net);
         
         if inM.mType = M_Success then
            if inM.response.peerNonce = p -- Make sure the message comes from the right server
            &  inM.response.serverNonce = peer[p].authenticator
            &  inM.response.password = p
            then -- check the peer challenge...
               peer[p].state := P_SUCCESS;
            else
               peer[p].state := P_BADAUTH;
            end;
         elsif inM.mType = M_Failure then
            error "peer was refused";
            peer[p].state := P_FAILURE;
         elsif inM.mType = M_Failure_Expired then
            -- Generate a new message, that has the password in it.
            undefine outM;
            outM.session.client := p;
            outM.session.server := peer[p].authenticator;
            outM.mType    := M_ChangePassword;
            outM.fromIntruder := false;
                  
            outM.serverNonce   := inM.serverNonce;
            outM.response.password := p;

            multisetadd (outM,net);
         end;
      end;
   end;
end;


------------------------------------------------------------------
--   ___       __  __            __  _          __              --
--  / _ |__ __/ /_/ /  ___ ___  / /_(_)______ _/ /____  _______ --
-- / __ / // / __/ _ \/ -_) _ \/ __/ / __/ _ `/ __/ _ \/ __(_-< --
--/_/ |_\_,_/\__/_//_/\__/_//_/\__/_/\__/\_,_/\__/\___/_/ /___/ --
--                                                              --
------------------------------------------------------------------
--AUTHENTICATORS

-- authenticator i reacts to peer's connect (step 2)
ruleset s: AuthenticatorId do
   choose m: net do
      rule "authenticator s reacts to peer's connect (step 2)"

         auth[s].state = A_SLEEP
         &  net[m].session.server = s -- make sure the message is for me
         &  net[m].fromIntruder -- all messages come from the intruder
         &  net[m].mType = M_Connect
      ==>

      var
         outM: Message;   -- outgoing message
         inM:  Message;   -- incoming message

      begin
         inM := net[m];
         multisetremove (m,net);

         undefine outM;
         outM.session.server  := s;
         outM.session.client  := inM.session.client;   -- identifier of peer
         outM.mType           := M_Challenge;
         outM.serverNonce     := s;
         outM.fromIntruder    := false;

         multisetadd (outM,net);

         auth[s].state     := A_WAIT_RESPONSE;
         auth[s].peer      := inM.session.client;
      end;
   end;
end;

-- authenticator s reacts to challenge response (step 4)
ruleset s: AuthenticatorId do
   choose m: net do
      rule "authenticator s reacts to challenge response (step 4)"

         auth[s].state = A_WAIT_RESPONSE
         &  net[m].session.server = s
         &  net[m].session.client = auth[s].peer
         &  net[m].mType = M_Response
         & net[m].fromIntruder

      ==>
      
      var
         inM: Message;
         outM: Message;

      begin
         alias p : auth[s].peer do
            inM := net[m];
            multisetremove (m,net);
         
            undefine outM;
            outM.fromIntruder := false;
            outM.session.server := s;
            outM.session.client := p;

   
         -- respond to peer challenge

            alias ntr: inM.response do
               if ntr.password = p
                  & ntr.peerNonce = inM.peerNonce
                  & ntr.password = p
                  & ntr.serverNonce = s
               then   -- correct hash received
                  auth[s].state := A_SUCCESS;
                  outM.mType := M_Success;
                  outM.response := ntr;
               else
                  auth[s].state := A_FAILURE;
                  outM.mType := M_Failure;
               end;
            end;
         end;
         multisetadd(outM, net);
      end;
   end;
end;

-- MESSAGES

choose m:net do
   rule "Message is lost..."
   net[m].fromIntruder  -- only remove messages that are not going to be
                        -- "eaten" by the intruder
   ==>
   begin
      multisetremove (m, net)
   end;
end;



---------------------------------------------
--   ____     __              __           --
--  /  _/__  / /_______ _____/ /__ _______ --
-- _/ // _ \/ __/ __/ // / _  / -_) __(_-< --
--/___/_//_/\__/_/  \_,_/\_,_/\__/_/ /___/ --
--                                         --
---------------------------------------------
--INTRUDERS


-- intruder i intercepts messages
ruleset i: IntruderId do
	choose m: net do
		rule "intruder intercepts"

			!net[m].fromIntruder    -- not for intruders' messages

		==>

		var
			msg: Message;

		begin
			msg:= net[m]; -- message to intercept

			-- all messages contain a session, except connect
			-- (even if in our model, it technically does as well)
			if(msg.mType != M_Connect) then
				int[i].sessions[msg.session.server][msg.session.client] := true;
			end;

			if (msg.mType = M_Challenge) then

				int[i].serverNonces[msg.serverNonce] := true;

			elsif (msg.mType = M_Response) then

				int[i].peerNonces[msg.session.client] := true;
				int[i].NTResponses[msg.response.peerNonce][msg.response.serverNonce][msg.response.password] := true;

			elsif (msg.mType = M_Success) then
			
				int[i].AuthResponses[msg.response.peerNonce][msg.response.serverNonce][msg.response.password] := true;
				
			elsif (msg.mType = M_ChangePassword) then
			
				int[i].passwords[msg.session.client] := true;
				
			end;
			multisetremove (m,net);
		end;
	end;
end;

-- Update some knowledge from other knowledge
ruleset i: IntruderId do
   ruleset p1: PeerIntruder do
	   ruleset p2: PeerIntruder do
	      ruleset s: AuthenticatorIntruder do
	         rule "Intruder creates NTResponse from pwdh, peerNonce, serverNonce"

	            int[i].passwords[p1]
  		      &  int[i].peerNonces[p2]
   	      &  int[i].serverNonces[s]
      	   &  !int[i].NTResponses[p2][s][p1] -- so that we only do it once
         	==>
         	begin
           	 	int[i].NTResponses[p2][s][p1] := true
         	end;
      	end;
		end;
   end;
end;

-- Update some knowledge from other knowledge
ruleset i: IntruderId do
	ruleset p1: PeerIntruder do
		ruleset p2: PeerIntruder do
			ruleset s: AuthenticatorIntruder do
				rule "Intruder creates AuthenticatorResponse from NTResponse, pwdh"

				   int[i].passwords[p1]
				&  int[i].NTResponses[p2][s][p1]
				& !int[i].AuthResponses[p2][s][p1] -- so that we only do it once
				==>
				begin
					int[i].AuthResponses[p2][s][p1] := true
				end;
			end;
		end;
	end;
end;

-- intruder i forges M_Connect message
ruleset i: IntruderId do
	ruleset p: PeerIntruder do           -- pick a peer to claim to be sending from
		ruleset s: AuthenticatorIntruder do -- pick a server to connect to
			rule "Intruder says hello!"
				multisetcount (l:net, true) < NetworkSize  -- only send a message if network is not full
			==>
			var
				outM:Message;
			begin
				undefine outM;
				outM.mType := M_Connect;
				outM.fromIntruder := true;
				outM.session.client := p;
				outM.session.server := s;
				multisetadd (outM,net);
			end;
		end;
	end;
end;

-- intruder i forges M_Challenge message
ruleset i: IntruderId do
	ruleset p: PeerIntruder do
		ruleset s1: AuthenticatorIntruder do -- challenge used
			ruleset s2: AuthenticatorIntruder do -- claimed source
				rule "Intruder sends M_Challenge"
					int[i].serverNonces[s1]
				& multisetcount (l:net, true) < NetworkSize  -- only send a message if network is not full
				& int[i].sessions[s2][p]
				==>
				var
					outM: Message;
				begin
					undefine outM;
					outM.mType := M_Challenge;
					outM.session.client := p;
					outM.session.server := s2;
					outM.serverNonce := s1;
					outM.fromIntruder := true;
					multisetadd(outM, net);
				end;
			end;
		end;
	end;
end;
         
-- intruder i forges M_Response message
ruleset i: IntruderId do
   ruleset response_peer_nonce_owner: PeerIntruder do
	   ruleset peer_password_owner: PeerIntruder do
		   ruleset claimed_peer: PeerIntruder do
		      ruleset response_server_nonce_owner: AuthenticatorIntruder do
			      ruleset destination: AuthenticatorId do
				      ruleset peer_nonce_owner: PeerIntruder do
	   			      rule "Intruder sends M_Response"
	      				 	multisetcount (l:net, true) < NetworkSize -- only send a message if network is not full
				         	&	int[i].NTResponses[response_peer_nonce_owner][response_server_nonce_owner][peer_password_owner]
							&	int[i].sessions[destination][claimed_peer]
							&	int[i].peerNonces[peer_nonce_owner]
							--&	int[i].passwords[peer_password_owner]
				         ==>
				         var
				            outM: Message;
				         begin
				            undefine outM;
				            outM.fromIntruder := true;
				            outM.mType := M_Response;
				            outM.session.client := claimed_peer;
				            outM.session.server := destination;
				            outM.peerNonce := peer_nonce_owner;
				            outM.response.peerNonce:= response_peer_nonce_owner;
				            outM.response.serverNonce:= response_server_nonce_owner;
				            outM.response.password := peer_password_owner;
				            multisetadd(outM, net);
				         end;
			         end;
		         end;
	         end;
         end;
      end;
   end;
end;

-- intruder i forges M_Success message
ruleset i: IntruderId do
   ruleset destination: PeerId do
   	ruleset response_peer_nonce_owner: PeerIntruder do
	   	ruleset peer_password_owner: PeerIntruder do
		      ruleset response_server_nonce_owner: AuthenticatorIntruder do
			      ruleset claimed_server: AuthenticatorIntruder do
   			      rule "Intruder sends M_Response"
     				 	 	multisetcount (l:net, true) < NetworkSize -- only send a message if network is not full
			         &  int[i].AuthResponses[response_peer_nonce_owner][response_server_nonce_owner][peer_password_owner]
						&	int[i].sessions[claimed_server][destination]
			         ==>
						var
							outM:Message;
						begin
			            undefine outM;
			            outM.fromIntruder := true;
			            outM.mType := M_Success;
			            outM.session.client := destination;
			            outM.session.server := claimed_server;
			            outM.response.peerNonce:= response_peer_nonce_owner;
			            outM.response.serverNonce:= response_server_nonce_owner;
			            outM.response.password := peer_password_owner;
			            multisetadd(outM, net);
						end;
					end;
				end;
			end;
		end;
	end;
end;

ruleset i: IntruderId do
	ruleset s: AuthenticatorIntruder do
		ruleset p: PeerId do
			rule "Intruder forges M_Failure_Expired"
            
				AttackerSendsFailure -- make sure this is legal
				&  multisetcount (l:net, true) < NetworkSize -- only send a message if network is not full
				& int[i].serverNonces[s]
				& int[i].sessions[s][p]
			==>
			var
				outM: Message;
			begin
				undefine outM;
				outM.fromIntruder := true;
				outM.session.client := p;
				outM.session.server := s;
				outM.serverNonce := s;
				outM.mType := M_Failure_Expired;
				multisetadd(outM, net);
			end;
		end;
	end;
end;


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

startstate
   -- initialize peers
   undefine peer;
   for p: PeerId do
      peer[p].state         := P_LINK;
      undefine peer[p].authenticator;
   end;
   -- initialize servers
   undefine auth;
   for s: AuthenticatorId do
      auth[s].state    := A_SLEEP;
      undefine auth[s].peer;
   end;

   -- initialize intruders
   undefine int;
   for i: IntruderId do   -- the only nonce known is the own one
      for j: PeerId do
         int[i].passwords[j] := false;
      end;
      for s: AuthenticatorIntruder do
         int[i].serverNonces[s] := false;
         for p1: PeerIntruder do
	         for p2: PeerIntruder do
  		         int[i].NTResponses[p1][s][p2] := false;
   	         int[i].AuthResponses[p1][s][p2] := false;
         	end;
	         int[i].sessions[s][p1] := false;
			end;
      end;
      int[i].AuthResponses[i][i][i] := true;
      int[i].NTResponses[i][i][i] := true;
      for p: PeerId do
         int[i].sessions[i][p] := true;
         int[i].peerNonces[p] := false;
      end;
      int[i].passwords[i] := true;
      int[i].serverNonces[i] := true;
      int[i].peerNonces[i] := true;
   end;

   -- initialize network 
   undefine net;
end;



------------------------------------------------
--   ____                  _           __     --
--  /  _/__ _  _____ _____(_)__ ____  / /____ --
-- _/ // _ \ |/ / _ `/ __/ / _ `/ _ \/ __(_-< --
--/___/_//_/___/\_,_/_/ /_/\_,_/_//_/\__/___/ --
--                                            --
------------------------------------------------


--------------------------------------------------------------------------------
-- Server Authentication:
--   Make sure that the client enters "SUCCESS" only with people who are
-- actually servers.
--------------------------------------------------------------------------------


invariant "server correctly authenticated"
forall i: PeerId do
   peer[i].state = P_SUCCESS &
   ismember(peer[i].authenticator, AuthenticatorId)
   
   ->
   !CheckServerAuth |
   auth[peer[i].authenticator].peer = i &
   auth[peer[i].authenticator].state = A_SUCCESS
end;

--------------------------------------------------------------------------------
-- Client Authentication:
--   Make sure that the server enters "SUCCESS" only with people who are
-- actually clients.
--------------------------------------------------------------------------------

invariant "peer correctly authenticated"
forall i: AuthenticatorId do
   auth[i].state = A_SUCCESS &
   ismember(auth[i].peer, PeerId)
   
   ->
   !CheckClientAuth |     
   peer[auth[i].peer].authenticator = i
end;


invariant "no peer passwords are known by intruders"
forall i: IntruderId do
   forall p: PeerId do
      true ->
      !int[i].passwords[p]
   end
end;
