--------------------------------------------------------------------------------
--
--  Murphi Model of the CHAP protocol, between Authenticator A end Peer P
--
--  MICROSOFT CHAP VERSION 2
--
--------------------------------------------------------------------------------
--
--  steps of the protocol modeled:
--
--   1. A->P: session + nonce
--   2. P->A: session + {session + password + nonce}hash
--   3. A->P: 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
  MaxKnowledge:   15;       -- max. number of messages intruder can remember
  
  -- Protocol modifiers
  CheckServerAuth:       true; -- true to ensure that client goes into success from a server
  CheckPeerAuth:         false; -- true to ensure that server authenticates right person
  
  AttackerCanChangeUser: true; -- true if attacker can change a message's username (claimed source)
  AttackerSendsFailure:  true; -- true if attacker sends password_expired to response instead of server's success
  AttackerFakesSuccess:  true; -- true if attacker can fake a success message from a client


-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-- Types defined for this MurPHI model.
type

	AuthenticatorId:  scalarset (NumAuthenticators);
	PeerId:           scalarset (NumPeers);
	IntruderId:       scalarset (NumIntruders);
  
	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
	};
	
	Session: record
		server:   AgentId;
		client:   AgentId;
	end;

	Message : record
		source:   AgentId;           -- source of message
		username: AgentId;           -- claimed source of message
		dest:     AgentId;           -- intended destination of message
		mType:    MessageType;       -- type of message
		session:  Session;           -- the id of the peer
		nonce1:   AgentId;           -- the nonce given to the linking peer
		nonce2:   AgentId;           -- the nonce given to the server by the peer (Peer Challenge)
		password: AgentId;           -- the password of a peer
	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: AgentId;               -- 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: AgentId;
	end;
	
	PeerArray : array[PeerId] of boolean;

	Intruder : record
		passwords:        array[AgentId] of boolean;   -- known passwords
		sessions: array[AuthenticatorId] of PeerArray;
		messages: multiset[MaxKnowledge] of Message;  -- known messages
	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



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



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


-- peer i starts protocol with server or intruder j (step 1)
ruleset i: PeerId do
	ruleset j: AgentId do
		rule 20 "peer sends Hello (step 1)"

			peer[i].state = P_LINK &
			!ismember(j, PeerId) &               -- only servers and intruders
			multisetcount (l:net, true) < NetworkSize  -- only send a message if network is not full

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

		begin
			undefine outM;
			outM.source  := i;
			outM.username:= i;
			outM.dest    := j;
			outM.mType   := M_Connect;
			--outM.session := undefined;
			--outM.nonce  := undefined;
			--outM.password := undefined;
			multisetadd (outM,net);

			peer[i].state         := P_WAIT_CHALLENGE;
			peer[i].authenticator := j;
		end;
	end;
end;

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

			peer[i].state = P_WAIT_CHALLENGE &
			net[j].dest = i &
			ismember(net[j].source,IntruderId) -- because everything goes through intruder
		==>

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

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

			if inM.username = peer[i].authenticator then   -- message comes from the right server

				if inM.mType = M_Challenge then   -- correct message type
					undefine outM;
					outM.source   := i;
					outM.dest     := peer[i].authenticator;
					outM.mType    := M_Response;
					outM.session.server  := inM.session.server;
					outM.session.client  := inM.session.client;
					outM.nonce1   := inM.nonce1;
					outM.password := i;
					outM.username := i;
					
					-- Peer challenge
					outM.nonce2 := i;

					multisetadd (outM,net);

					peer[i].state := P_WAIT_OK;
				end;

			end;
		end;
	end;
end;

-- peer receives a success or failure message
ruleset i: PeerId do
	choose j: net do
		rule 20 "peer receives success/failure (step 5)"
		
			peer[i].state = P_WAIT_OK &
			net[j].dest = i &
			ismember(net[j].source,IntruderId) -- because everything goes through intruder
		==>
		
		var
			inM: Message; -- incoming
			outM: Message; -- potential outgoing
		
		begin
			inM := net[j];
			multisetremove(j, net);
			
			if inM.username = peer[i].authenticator then
				if inM.session.server = peer[i].authenticator & -- check the session...
				inM.session.client = i then
					if inM.mType = M_Success then
						if inM.nonce2 = i then -- check the peer challenge...
							peer[i].state := P_SUCCESS;
						else
							peer[i].state := P_BADAUTH;
						end
					elsif inM.mType = M_Failure then
						error "peer was refused";
						peer[i].state := P_FAILURE;
					elsif inM.mType = M_Failure_Expired then
						-- Generate a new message, that has the password in it.
						undefine outM;
						outM.source   := i;
						outM.dest     := peer[i].authenticator;
						outM.mType    := M_ChangePassword;
						
						outM.session.server  := inM.session.server;
						outM.session.client  := inM.session.client;
						outM.nonce1   := inM.nonce1;
						outM.password := i;
						outM.username := i;

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


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

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


			auth[i].state = A_SLEEP &
			net[j].dest = i &
			ismember(net[j].source,IntruderId)

		==>

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

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

			if inM.mType = M_Connect then   -- correct message type
				undefine outM;
				outM.source   := i;
				outM.dest     := inM.username;   -- identifier of peer
				outM.mType    := M_Challenge;
				outM.session.server  := i;
				outM.session.client  := inM.username;
				outM.nonce1   := inM.username;
				outM.username := i;
				--outM.password := undefined;

				multisetadd (outM,net);

				auth[i].state     := A_WAIT_RESPONSE;
				auth[i].peer := inM.username;
			end;

		end;
	end;
end;

-- authenticator i reacts to challenge response (step 4)
ruleset i: AuthenticatorId do
	choose j: net do
		rule 20 "authenticator i reacts to challenge response (step 4)"

			auth[i].state = A_WAIT_RESPONSE &
			net[j].dest = i &
			ismember(net[j].source,IntruderId)

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

		begin
			inM := net[j];
			multisetremove (j,net);
			
			if inM.session.server = i & inM.session.client = inM.username then   -- message is has j's session ID
				if inM.mType = M_Response then   -- correct message type
					if inM.nonce1 = inM.username then    -- correct challenge id (nonce) received
						undefine outM;
						outM.source := i;
						outM.dest := inM.username;
						outM.session := inM.session;
						outM.nonce1 := inM.username;
						outM.username := i;
						
						-- respond to peer challenge
						outM.nonce2 := inM.nonce2;
						--outM.password := undefined;
						
						if inM.password = inM.username then   -- correct password received
							auth[i].state := A_SUCCESS;
							outM.mType := M_Success;
						else
							auth[i].state := A_FAILURE;
							outM.mType := M_Failure;
						end;
						
						multisetadd(outM, net);
					end;
				end;
			end;

		end;
	end;
end;


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

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

			!ismember (net[j].source, IntruderId)    -- not for intruders' messages

		==>

		var
			temp: Message;

		begin
			alias msg: net[j] do   -- message to intercept

				alias messages: int[i].messages do
					temp := msg;
					undefine temp.source;   -- delete useless information
					undefine temp.dest;
					if multisetcount (l:messages,   -- add only if not there
					messages[l].mType = temp.mType &
					messages[l].nonce1 = temp.nonce1 &
					messages[l].nonce2 = temp.nonce2 &
					messages[l].session.server = temp.session.server &
					messages[l].session.client = temp.session.client &
					messages[l].username = temp.username &
					messages[l].password = temp.password ) = 0
						then
							multisetadd (temp, int[i].messages);
					end;
				end;

				multisetremove (j,net);
			end;
		end;
	end;
end;

-- intruder i sees a challenge message

ruleset i: IntruderId do
	choose j: net do
		rule 10 "intruder sees challenge message (nonce + session in clear)"
			ismember( net[j].source, AuthenticatorId) &
			ismember( net[j].dest, PeerId) &
			net[j].mType = M_Challenge
		==>
		begin
			int[i].sessions[net[j].source][net[j].dest] := true;
		end;
	end;
end;


ruleset i: IntruderId do
	choose m: net do
		rule 10 "intruder intercepts response, sends password expired"
			
			AttackerSendsFailure & -- make sure this is legal
			
			ismember(net[m].source, PeerId) &
			ismember(net[m].dest, AuthenticatorId) &
			net[m].mType = M_Response
		
		==>
		var
			outM: Message;
			inM:  Message;
		begin
			inM := net[m];
			
			undefine outM;
			outM.source := i;
			outM.dest := inM.username;
			outM.session := inM.session;
			outM.nonce1 := inM.username;
			outM.username := inM.dest; -- make the message appear to come from server
					
			outM.mType := M_Failure_Expired;
			multisetremove(m, net);
			multisetadd(outM, net);
		end;
	end;
end;


-- intruder i sends recorded message
ruleset i: IntruderId do         -- arbitrary choice of
	choose j: int[i].messages do     --  recorded message
		ruleset k: AgentId do    --  destination
			rule 90 "intruder sends recorded message"

				!ismember(k, IntruderId) &                 -- not to intruders
				multisetcount (l:net, true) < NetworkSize

			==>

			var
				outM: Message;

			begin
				outM          := int[i].messages[j];
				outM.source   := i;
				outM.dest     := k;
				outM.username := int[i].messages[j].username;

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

ruleset i: IntruderId do         -- arbitrary choice of
	choose j: int[i].messages do     --  recorded message
		ruleset u: AgentId do        --  claimed source
			ruleset k: AgentId do    --  destination
				rule 90 "intruder sends recorded message with new username"

					AttackerCanChangeUser &                      -- make sure the rule is enabled
					!ismember(k, IntruderId) &                 -- not to intruders
					!ismember(u, AuthenticatorId) &            -- not from servers
					int[i].messages[j].username != u &         -- not same username
					multisetcount (l:net, true) < NetworkSize

				==>

				var
					outM: Message;

				begin
					outM        := int[i].messages[j];
					outM.source := i;
					outM.dest   := k;

					outM.username := u;

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

-- intruder i fakes response to Peer Response
ruleset i: IntruderId do
	choose m: net do
		rule 10 "intruder fakes response to Peer Response"
		
			AttackerFakesSuccess &

			ismember(net[m].source, PeerId) & -- from a peer...
			ismember(net[m].dest, AuthenticatorId) & -- to an authenticator

			net[m].mType = M_Response -- only for a response message
		==>

		var
			outM: Message;
			inM: Message;
		begin
			inM := net[m];
			
			undefine outM;
			outM.source := i;
			outM.dest := inM.username;
			outM.session := inM.session;
			outM.nonce1 := inM.nonce1;

			-- Intruder cannot set nonce2, because nonce2 is created by hashing
			-- Auth-Challenge, Peer-Challenge, Hashed-Peer-Password, and Peer-Password.
			-- The intruder has everything but the cleartext peer password.
			outM.nonce2 := undefined;

			outM.username := inM.dest; -- make the message appear to come from server

			outM.mType := M_Success;
			multisetremove(m, net);
			multisetadd(outM, net);
		end;
	end;
end;

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

startstate
	-- initialize peers
	undefine peer;
	for i: PeerId do
		peer[i].state         := P_LINK;
		peer[i].authenticator := i;
	end;

	-- initialize servers
	undefine auth;
	for i: AuthenticatorId do
		auth[i].state    := A_SLEEP;
		auth[i].peer     := i;
	end;

	-- initialize intruders
	undefine int;
	for i: IntruderId do   -- the only nonce known is the own one
		for j: AgentId do  
			int[i].passwords[j] := false;
		end;
		for j: AuthenticatorId do
			for k: PeerId do
				int[i].sessions[j][k] := false;
			end;
		end;
		int[i].passwords[i] := true;
	end;

	-- initialize network 
	undefine net;
end;



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

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
;

-- "server talks to peer who is talking to same server"
invariant "server authenticates only peers connecting to it"
	forall i: AuthenticatorId do
		auth[i].state = A_SUCCESS &
		ismember(auth[i].peer, PeerId)
		
		->

		!CheckPeerAuth |		
		peer[auth[i].peer].authenticator = i
	end
;
	
invariant "no peer passwords are known by intruders"
	forall i: IntruderId do
		forall j: AgentId do
			ismember(j, PeerId)
			->
			int[i].passwords[j] = false
		end
	end
;

