-------------------------------------------------------------------------------- -- -- Murphi Model of the Kerberos Protocol Version 5 (simplified) -- -------------------------------------------------------------------------------- -- -- version: 1.0 -- -- written by: Ulrich Stern -- date: Oct 1996 -- affiliation: Stanford University (visiting scholar), -- Technical University of Munich (PhD student) -- -------------------------------------------------------------------------------- -- -- simplifications: -- no nonces -- no timestamp -- no unencrypted server in ticket -- -- resulting protocol: -- -- Client->KDC : c, tgs -- KDC ->Client: {Kc_tgs}Kc, Tc_tgs -- Client->TGS : Ac_tgs, Tc_tgs, s -- TGS ->Client: {Kc_s}Kc_tgs, Tc_s -- Client->Server: Ac_s, Tc_s -- -- c: client s: server tgs: ticket-granting server -- KDC: Key Distribution Center -- ticket: Tc_s = {c,Kc_s}Ks Kc_s: session key -- authenticator: Ac_s = {c}Kc_s -- -- reference: -- J.T. Kohl, B.C. Neuman, T.Y. Ts'o -- The Evolution of the Kerberos Authentication Service -- Distributed Open Systems, 1994. -- http://nii.isi.edu/people/bcn/publications.html -- -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -- constants, types and variables -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- const NumClients: 1; NumServers: 1; NumKDCs: 1; NumTGSs: 1; NumIntruders: 1; NetworkSize: 1; -- max. number of outstanding messages in network MaxTickets: 10; -- max. number of tickets intruder can remember MaxAuthen: 10; -- authenticators MaxEnKeys: 10; -- encrypted keys Max_M_Id: 1; -- max. number of M_Id messages intruder can send Max_M_KT: 2; -- M_KT messages Max_M_AT: 1; -- M_AT messages Max_M_ATI: 1; -- M_ATI messages MaxKeys: 5; -- max. number of session keys -------------------------------------------------------------------------------- type ClientId: scalarset (NumClients); -- identifiers ServerId: scalarset (NumServers); KDCId: scalarset (NumKDCs); TGSId: scalarset (NumTGSs); IntruderId: scalarset (NumIntruders); AgentId: union {ClientId, ServerId, KDCId, TGSId, IntruderId}; -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- messages MessageType : enum { -- different types of messages M_Id, -- id M_KT, -- encrypted key, ticket M_AT, -- authenticator, ticket M_ATI -- authenticator, ticked, id }; KeyType : enum { K_Secret, K_Session }; SessionKeyId : 1..MaxKeys; Key : record kType: KeyType; id: AgentId; no: SessionKeyId; end; Ticket : record id: AgentId; key1: Key; key2: Key; end; Authenticator : record id: AgentId; key: Key; end; EnKey : record -- encrypted session key key1: Key; key2: Key; end; Message : record source: AgentId; -- source of message dest: AgentId; -- intended destination of message mType: MessageType; id1: AgentId; -- constituent parts of message id2: AgentId; ticket: Ticket; authen: Authenticator; enKey: EnKey; end; -- message encoding: -- M_Id: id1,id2 -- M_KT: enKey, ticket -- M_AT: authen, ticket -- M_ATI: authen, ticket, id1 -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- client ClientStates : enum { C_SLEEP, -- state after initialization C_WAIT_KDC, -- waiting for response from KDC C_WAIT_TGS, -- waiting for response from TGS C_DONE -- after ticket sent to server }; Client : record state: ClientStates; server: AgentId; -- server which client wants to contact sKey: SessionKeyId; -- session key for that contact end; -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- server ServerStates : enum { S_SLEEP, S_COMMIT }; Server : record state: ServerStates; client: AgentId; sKey: SessionKeyId; end; -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- intruder Intruder : record keys: array[SessionKeyId] of boolean; -- known session keys tickets: multiset[MaxTickets] of Ticket; -- tickets authen: multiset[MaxAuthen] of Authenticator; -- authenticators enKeys: multiset[MaxEnKeys] of EnKey; -- encrypted keys no_M_Id: 1..Max_M_Id; -- no. of next message no_M_KT: 1..Max_M_KT; -- to send no_M_AT: 1..Max_M_AT; no_M_ATI: 1..Max_M_ATI; end; -- remark: KDC and TGS are stateless -------------------------------------------------------------------------------- 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: SessionKeyId; -- next session key -------------------------------------------------------------------------------- -- procedures and functions -------------------------------------------------------------------------------- -- generate next session key function GenSessionKey(): SessionKeyId; var r: SessionKeyId; begin if isundefined(nextKey) then error "out of session 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 message to KDC j requesting ticket for TGS k ruleset i: ClientId do ruleset j: KDCId do ruleset k: TGSId do rule "client sends message to KDC" cli[i].state = C_SLEEP & multisetcount (l:net, true) < NetworkSize ==> var outM: Message; -- outgoing message begin undefine outM; outM.source := i; outM.dest := j; outM.mType := M_Id; outM.id1 := i; outM.id2 := k; multisetadd (outM,net); cli[i].state := C_WAIT_KDC; cli[i].server := k; -- store id of TGS end; end; end; end; -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- client i sends message to TGS requesting ticket for server k ruleset i: ClientId do ruleset k: ServerId do choose l: net do rule "client sends message to TGS" cli[i].state = C_WAIT_KDC & net[l].dest = i ==> var inM: Message; -- incoming message outM: Message; -- outgoing message begin inM := net[l]; multisetremove (l,net); if inM.mType=M_KT & -- correct message type inM.enKey.key2.kType=K_Secret & -- correct secret key inM.enKey.key2.id=i then undefine outM; outM.source := i; outM.dest := cli[i].server; outM.mType := M_ATI; outM.authen.id := i; -- authenticator outM.authen.key := inM.enKey.key1; outM.ticket := inM.ticket; -- ticket outM.id1 := k; -- id multisetadd (outM,net); cli[i].state := C_WAIT_TGS; cli[i].server := k; cli[i].sKey := inM.enKey.key1.no; end; end; end; end; end; -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- client i sends message to server ruleset i: ClientId do choose j: net do rule "client sends message to server" cli[i].state = C_WAIT_TGS & net[j].dest = i ==> var inM: Message; -- incoming message outM: Message; -- outgoing message begin inM := net[j]; multisetremove (j,net); if inM.mType=M_KT & -- correct message type inM.enKey.key2.kType=K_Session & -- correct secret key inM.enKey.key2.no=cli[i].sKey then undefine outM; outM.source := i; outM.dest := cli[i].server; outM.mType := M_AT; outM.authen.id := i; -- authenticator outM.authen.key := inM.enKey.key1; outM.ticket := inM.ticket; -- ticket multisetadd (outM,net); cli[i].state := C_DONE; cli[i].sKey := inM.enKey.key1.no; end; end; end; end; -------------------------------------------------------------------------------- -- behavior of KDCs and TGSs -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- KDC i sends message to client ruleset i: KDCId do choose j: net do rule "KDC sends message to client" net[j].dest = i ==> var outM: Message; -- outgoing message inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); if inM.mType=M_Id then -- correct message type undefine outM; outM.source := i; outM.dest := inM.id1; outM.mType := M_KT; outM.enKey.key1.kType := K_Session; -- key outM.enKey.key1.no := GenSessionKey(); outM.enKey.key2.kType := K_Secret; outM.enKey.key2.id := inM.id1; outM.ticket.id := inM.id1; -- ticket outM.ticket.key1 := outM.enKey.key1; outM.ticket.key2.kType := K_Secret; outM.ticket.key2.id := inM.id2; multisetadd (outM,net); end; end; end; end; -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- TGS i sends message to client ruleset i: TGSId do choose j: net do rule "TGS sends message to client" net[j].dest = i ==> var outM: Message; -- outgoing message inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); if inM.mType=M_ATI & -- correct message type inM.ticket.key2.kType=K_Secret & -- able to decrypt ticket inM.ticket.key2.id=i & inM.ticket.key1.kType=K_Session & -- able to decrypt authenticator inM.authen.key.kType=K_Session & inM.authen.key.no=inM.ticket.key1.no & inM.authen.id=inM.ticket.id then -- authenticator correct undefine outM; outM.source := i; outM.dest := inM.ticket.id; outM.mType := M_KT; outM.enKey.key1.kType := K_Session; -- key outM.enKey.key1.no := GenSessionKey(); outM.enKey.key2 := inM.ticket.key1; outM.ticket.id := inM.ticket.id; -- ticket outM.ticket.key1 := outM.enKey.key1; outM.ticket.key2.kType := K_Secret; outM.ticket.key2.id := inM.id1; multisetadd (outM,net); end; end; end; end; -------------------------------------------------------------------------------- -- behavior of servers -- server i receives message from client ruleset i: ServerId do choose j: net do rule "server receives message from client" net[j].dest = i ==> var outM: Message; -- outgoing message inM: Message; -- incoming message begin inM := net[j]; multisetremove (j,net); if inM.mType=M_AT & -- correct message type inM.ticket.key2.kType=K_Secret & -- able to decrypt ticket inM.ticket.key2.id=i & inM.ticket.key1.kType=K_Session & -- able to decrypt authenticator inM.authen.key.kType=K_Session & inM.ticket.key1.no=inM.authen.key.no & inM.ticket.id=inM.authen.id then -- authenticator correct ser[i].state := S_COMMIT; ser[i].client := inM.ticket.id; ser[i].sKey := inM.ticket.key1.no; 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 intruders' messages ==> begin alias msg: net[j] do -- message to overhear/intercept -- learn tickets if msg.mType=M_KT | msg.mType=M_AT | msg.mType=M_ATI then if msg.ticket.key2.id=i then -- intruder can decrypt int[i].keys[msg.ticket.key1.no] := true; -- learn session key else -- store ticket alias tickets: int[i].tickets do if multisetcount (l:tickets, -- check if already there tickets[l].id = msg.ticket.id & tickets[l].key1.no = msg.ticket.key1.no & tickets[l].key2.id = msg.ticket.key2.id ) = 0 then multisetadd (msg.ticket, tickets); end; end; end; end; -- learn authenticators if msg.mType=M_AT | msg.mType=M_ATI then alias authen: int[i].authen do if multisetcount (l:authen, authen[l].id = msg.authen.id & authen[l].key.no = msg.authen.key.no ) = 0 then multisetadd (msg.authen, authen); end; end; end; -- learn encrypted keys if msg.mType=M_KT then if (msg.enKey.key2.kType=K_Secret & -- decrypt msg.enKey.key2.id=i) | (msg.enKey.key2.kType=K_Session & int[i].keys[msg.enKey.key2.no]) then int[i].keys[msg.enKey.key1.no] := true; else -- store alias enKeys: int[i].enKeys do if multisetcount (l:enKeys, enKeys[l].key1.no = msg.enKey.key1.no & ( enKeys[l].key2.kType = K_Secret -> enKeys[l].key2.id = msg.enKey.key2.id ) & ( enKeys[l].key2.kType = K_Session -> enKeys[l].key2.no = msg.enKey.key2.no ) ) = 0 then multisetadd (msg.enKey, enKeys); end; end; end; end; -- intercept if intercept then multisetremove (j,net); end; end; end; end; end; end; -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- remark: it is sufficient if the intruder sends its generated messages only -- to agents that understand the corresponding message type. Otherwise, the -- message is just discarded. -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- intruder i generates M_Id message ruleset i: IntruderId do -- arbitrary choice of ruleset j: KDCId do -- destination ruleset k: AgentId do -- client ruleset l: TGSId do -- TGS rule "intruder generates M_Id message" !isundefined(int[i].no_M_Id) & (ismember (k, ClientId) | -- only clients or intruders ismember (k, IntruderId)) & multisetcount (z:net, true) < NetworkSize ==> var outM: Message; begin undefine outM; outM.source := i; outM.dest := j; outM.mType := M_Id; outM.id1 := k; outM.id2 := l; multisetadd (outM,net); if int[i].no_M_Id < Max_M_Id then int[i].no_M_Id := int[i].no_M_Id+1; else undefine int[i].no_M_Id; end; end; end; end; end; end; -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- intruder i generates M_KT message -- remark: in the following, four cases have to be distinguished since the -- choose construct only enables the rule if there is at least one element -- in the multiset -- remark2: alternatively, one might insert a dummy element in the multiset -- and check not to use this dummy element, which would enable the use of -- only one (large) rule, but have a bad effect on the run-time -- replay key, replay ticket ruleset i: IntruderId do -- arbitrary choice of ruleset j: ClientId do -- destination choose k: int[i].enKeys do -- key choose l: int[i].tickets do -- ticket rule "intruder generates M_KT message" !isundefined(int[i].no_M_KT) & multisetcount (z:net, true) < NetworkSize ==> var outM: Message; begin undefine outM; outM.source := i; outM.dest := j; outM.mType := M_KT; outM.enKey := int[i].enKeys[k]; outM.ticket := int[i].tickets[l]; multisetadd (outM,net); if int[i].no_M_KT < Max_M_KT then int[i].no_M_KT := int[i].no_M_KT+1; else undefine int[i].no_M_KT; end; end; end; end; end; end; -- replay key, generate ticket -- generate key, generate ticket -- remark: cases seem not to be needed, since nobody (except intruders) could -- do anything with the resulting tickets which would be encrypted with -- intruder i's secret key. The corresponding cases are also negligible -- for M_AT and M_ATI messages. -- generate key, replay ticket ruleset i: IntruderId do -- arbitrary choice of ruleset j: ClientId do -- destination choose l: int[i].tickets do -- ticket ruleset m: SessionKeyId do -- encrypted session key ruleset n: SessionKeyId do -- session key used for encryption rule "intruder generates M_KT message" !isundefined(int[i].no_M_KT) & int[i].keys[m] & int[i].keys[n] & multisetcount (z:net, true) < NetworkSize ==> var outM: Message; begin undefine outM; outM.source := i; outM.dest := j; outM.mType := M_KT; outM.enKey.key1.kType := K_Session; outM.enKey.key1.no := m; outM.enKey.key2.kType := K_Session; outM.enKey.key2.no := n; outM.ticket := int[i].tickets[l]; multisetadd (outM,net); if int[i].no_M_KT < Max_M_KT then int[i].no_M_KT := int[i].no_M_KT+1; else undefine int[i].no_M_KT; end; end; end; end; end; end; end; -- remark: only session keys are used here to encrypt the transmitted key. -- Otherwise the resulting messages would be discarded be everyone but the -- intruders. -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- intruder i generates M_AT message -- replay authenticator, replay ticket ruleset i: IntruderId do -- arbitrary choice of ruleset j: ServerId do -- destination choose k: int[i].authen do -- authenticator choose l: int[i].tickets do -- ticket rule "intruder generates M_AT message" !isundefined(int[i].no_M_AT) & multisetcount (z:net, true) < NetworkSize ==> var outM: Message; begin undefine outM; outM.source := i; outM.dest := j; outM.mType := M_AT; outM.authen := int[i].authen[k]; outM.ticket := int[i].tickets[l]; multisetadd (outM,net); if int[i].no_M_AT < Max_M_AT then int[i].no_M_AT := int[i].no_M_AT+1; else undefine int[i].no_M_AT; end; end; end; end; end; end; -- generate authenticator, replay ticket ruleset i: IntruderId do -- arbitrary choice of ruleset j: ServerId do -- destination ruleset k: AgentId do -- id in authenticator ruleset n: SessionKeyId do -- key for authenticator choose l: int[i].tickets do -- ticket rule "intruder generates M_AT message" !isundefined(int[i].no_M_AT) & (ismember (k, ClientId) | ismember (k, IntruderId)) & int[i].keys[n] & multisetcount (z:net, true) < NetworkSize ==> var outM: Message; begin undefine outM; outM.source := i; outM.dest := j; outM.mType := M_AT; outM.authen.id := k; outM.authen.key.kType := K_Session; outM.authen.key.no := n; outM.ticket := int[i].tickets[l]; multisetadd (outM,net); if int[i].no_M_AT < Max_M_AT then int[i].no_M_AT := int[i].no_M_AT+1; else undefine int[i].no_M_AT; end; end; end; end; end; end; end; -- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -- intruder i generates M_ATI message -- remark: the M_ATI messages are very similar to the M_AT messages, so a -- single rule could be used. However, the run-time was very long in this -- case. -- replay authenticator, replay ticket ruleset i: IntruderId do -- arbitrary choice of ruleset j: TGSId do -- destination choose k: int[i].authen do -- authenticator choose l: int[i].tickets do -- ticket ruleset m: AgentId do -- server in M_ATI message rule "intruder generates M_ATI message" !isundefined(int[i].no_M_ATI) & (ismember (m, ServerId) | ismember (m, TGSId)) & multisetcount (z:net, true) < NetworkSize ==> var outM: Message; begin undefine outM; outM.source := i; outM.dest := j; outM.mType := M_ATI; outM.id1 := m; outM.authen := int[i].authen[k]; outM.ticket := int[i].tickets[l]; multisetadd (outM,net); if int[i].no_M_ATI < Max_M_ATI then int[i].no_M_ATI := int[i].no_M_ATI+1; else undefine int[i].no_M_ATI; end; end; end; end; end; end; end; -- generate authenticator, replay ticket ruleset i: IntruderId do -- arbitrary choice of ruleset j: TGSId do -- destination ruleset k: AgentId do -- id in authenticator ruleset n: SessionKeyId do -- key for authenticator choose l: int[i].tickets do -- ticket ruleset m: AgentId do -- server in M_ATI message rule "intruder generates M_ATI message" !isundefined(int[i].no_M_ATI) & (ismember (m, ServerId) | ismember (m, TGSId)) & (ismember (k, ClientId) | ismember (k, IntruderId)) & int[i].keys[n] & multisetcount (z:net, true) < NetworkSize ==> var outM: Message; begin undefine outM; outM.source := i; outM.dest := j; outM.mType := M_ATI; outM.id1 := m; outM.authen.id := k; outM.authen.key.kType := K_Session; outM.authen.key.no := n; outM.ticket := int[i].tickets[l]; multisetadd (outM,net); if int[i].no_M_ATI < Max_M_ATI then int[i].no_M_ATI := int[i].no_M_ATI+1; else undefine int[i].no_M_ATI; end; end; 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: SessionKeyId do int[i].keys[j] := false; end; int[i].no_M_Id := 1; int[i].no_M_KT := 1; int[i].no_M_AT := 1; int[i].no_M_ATI := 1; end; -- initialize network undefine net; -- initialize session key generator nextKey := 1; end; -------------------------------------------------------------------------------- -- invariants -------------------------------------------------------------------------------- invariant "client correctly authenticated" forall i: ServerId do ser[i].state = S_COMMIT & ismember(ser[i].client, ClientId) -> cli[ser[i].client].server = i & cli[ser[i].client].state = C_DONE end; invariant "test" forall i: ServerId do ser[i].state = S_COMMIT -> !ismember(ser[i].client, IntruderId) | true -- deleting this line will show an error trace in which the -- intruder acts as a client end;