theory Kerberos_V4 begin section{* The Kerberos Protocol, Version 4 *} text{* Modeled after the description given by Bella [1] based on the original technical report [2]. Notable differences: 1. We do not model the timestamps and the timing properties because our model does not support reasoning about them yet. We model them as freshly generated nonces that are leaked immediately after generation. 2. We do not model session key leakage, as our support for key compromise properties is not ready yet. 3. We provide more general authentication and secrecy properties, as we do not assume a priory the uncompromisedness of the ticket granting server. Furthermore, the authentication propertis are more fine-grained due to our more precise execution model. 4. We use explicit global constants instead of implicit typing to identify the different encryptions. 5. We use the abbreviations: C for Client, A for authenticator, G for ticket granting server, S for server. [1] Bella, Giampaolo and Paulson, Lawrence C., "Kerberos Version 4: Inductive Analysis of the Secrecy Goals", in ESORICS, 1998, pp. 361-375. [2] Miller, S. P. and Neuman, B. C. and Schiller, J. I. and Saltzer, J. H., "Kerberos Authentication and Authorization System", in Project Athena Technical Plan, 1987, pp. 1-36. *} protocol Kerberos { 1_leak. C -> : Tc1 1. C -> A: C,G,Tc1 2_leak. A -> : Ta 2. <- A: A, {'21', AuthKey, G, Ta, {'22', C, G, AuthKey, Ta}k(A,G) }k(C,A) C <- : A, {'21', AuthKey, G, Ta, AuthTicket }k(C,A) 3_leak. C -> : Tc2 3. C -> : A, AuthTicket, {'3', C, Tc2}AuthKey, S -> G: A, {'22', C, G, AuthKey, Ta}k(A,G), {'3', C, Tc2}AuthKey, S 4_leak. G -> : Tg 4. <- G: {'41', ServKey, S, Tg, {'42', C, S, ServKey, Tg}k(G,S) }AuthKey C <- : {'41', ServKey, S, Tg, ServTicket }AuthKey 5_leak. C -> : Tc3 5. C -> : G, ServTicket, {'5', C, Tc3}ServKey -> S: G, {'42', C, S, ServKey, Tg}k(G,S), {'5', C, Tc3}ServKey 6. C <- S: {'6', Tc3}ServKey } // The type inference heuristic is wrong for the type of ServTicket@C // Therefore, we had to modify its output to the following type. property (of Kerberos) Kerberos_typing: "// client variables A@C :: Known(C_2) AuthKey@C :: Known(C_2) | AuthKey@A ServKey@C :: Known(C_4) | ServKey@G Ta@C :: Known(C_2) | Ta@A Tg@C :: Known(C_4) | Tg@G AuthTicket@C :: Known(C_2) | {'22', Known(C_2), Agent, AuthKey@A, Ta@A}k(Agent, Agent) ServTicket@C :: Known(C_4) | {'42', Known(C_4), Agent, ServKey@G, Tg@G}k(Agent, Agent) // authenticator variables C@A :: Known(A_1) G@A :: Known(A_1) Tc1@A :: Known(A_1) // ticket granting server variables A@G :: Known(G_3) C@G :: Known(G_3) | Agent S@G :: Known(G_3) AuthKey@G :: Known(G_3) | AuthKey@A Ta@G :: Known(G_3) | Ta@A Tc2@G :: Known(G_3) | Tc2@C // server variables C@S :: Known(S_5) | Agent G@S :: Known(S_5) ServKey@S :: Known(S_5) | ServKey@G Tg@S :: Known(S_5) | Tg@G Tc3@S :: Known(S_5) | Tc3@C " subsection{* Secrecy Properties *} properties (of Kerberos) A_AuthKey_secret: secret(A, -, AuthKey, {C,A,G}) C_AuthKey_secret: secret(C, 2, AuthKey, {C,A,G}) G_AuthKey_secret: secret(G, 3, AuthKey, {C,A,G}) G_ServKey_sec: secret(G, -, ServKey, {C,A,G,S}) C_ServKey_sec: secret(C, 4, ServKey, {C,A,G,S}) // no secrecy for ServKey at server S because it cannot verify the // uncompromisedness of A subsection{* Authentication Properties *} // client property (of Kerberos) C_auth: premises "role(1) = C" "uncompromised(C#1, A#1, G#1, S#1)" "step(1, C_6)" imply threads 2, 3, 4 such that " // consequence from exchange with authenticator role(2) = A & A#1 = A#2 & C#1 = C#2 & G#1 = G#2 & Ta#1 = Ta#2 & AuthKey#1 = AuthKey#2 & // consequence from exchange with ticket granting server role(3) = G & A#1 = A#3 & C#1 = C#3 & G#1 = G#3 & S#1 = S#3 & Tg#1 = Tg#3 & AuthKey#1 = AuthKey#3 & ServKey#1 = ServKey#3 & // consequence from exchange with server role(4) = S & C#1 = C#4 & G#1 = G#4 & S#1 = S#4 & Tc3#1 = Tc3#4 & ServKey#1 = ServKey#4 " // ticket granting server property (of Kerberos) G_auth: premises "role(3) = G" "uncompromised(C#3, A#3, G#3)" "step(3, G_3)" imply threads 1, 2 such that " // consequence from receiving from client role(1) = C & A#1 = A#3 & C#1 = C#3 & G#1 = G#3 & Tc2#1 = Tc2#3 & AuthKey#1 = AuthKey#3 & // no agreement on ServKey and S as they are not guaranteed to have been // received by the client yet. // consequence of client receiving from authenticator role(2) = A & A#1 = A#2 & C#1 = C#2 & G#1 = G#2 & AuthKey#1 = AuthKey#2 " /* text{* Here we can only formulate a weaker authentication property because the uncompromisedness of the authenticator cannot be verified directly by the server. What we can prove is under the assumption that we got our ServKey from some ticket granting server and this server was talking to an uncompromised authenticator, then we have sort of an authentication. *} property (of Kerberos) S_auth: premises "role(4) = S" "uncompromised(C#4, S#4, G#4)" "step(4, S_5)" "role(3) = G" "uncompromised(A#3)" "ServKey#4 = ServKey#3" imply threads 1, 2 such that " // consequence from exchange with authenticator role(1) = C & role(2) = A & A#1 = A#2 & C#1 = C#2 & G#1 = G#2 & AuthKey#1 = AuthKey#2 & // consequence from exchange with ticket granting server A#1 = A#3 & C#1 = C#3 & G#1 = G#3 & S#1 = S#3 & AuthKey#1 = AuthKey#3 & ServKey#1 = ServKey#3 & // consequence from exchange with client C#1 = C#4 & G#1 = G#4 & S#1 = S#4 & t#1 = t#4 & ServKey#1 = ServKey#4 & // ordering consequences St(1, C_1) < St(2, A_1) < St(2, A_2) < St(1, C_2) < St(1, C_3) < St(3, T_3) < St(3, T_4) < St(1, C_4) < St(1, C_5) < St(4, S_5) " */ end