Kerberos is a distributed authentication service that allows a process (a client) running on behalf of a principal (a user) to prove its identity to a verifier (an application server, or just server) without sending data across the network that might allow an attacker or the verifier to subsequently impersonate the principal. Kerberos optionally provides integrity and confidentiality for data sent between the client and server.
C: Client A: Authentication Server G: Ticket Granting Server S: Server (that the client wants to talk to)K_AB: key shared or intended to be shared between A and B Initially shared: K_CA, K_AG, K_GS Established during protocol: K_CG, K_CS
All things marked * are timestamp-related and will be simply replaced with fresh text.
Macros: Ticket_1 := { C,G, K_CG, Tstart*, Texpire* }K_AG Ticket_2 := { C,S, K_CS, Tstart2*, Texpire2* }K_GS
1. C -> A : C,G,Lifetime_1*,N_1 2. A -> C : C, Ticket_1, { G, K_CG, Tstart*, Texpire*, N_1 }K_CA
3. C -> G : S,Lifetime_2*,N_2,Ticket_1, { C,T* }K_CG 4. G -> C : C, Ticket_2, { S, K_CS, Tstart2*, Texpire2*, N_2 }K_CG
5. C -> S : Ticket_2, { C, T2* }K_CS 6. S -> C : { T2* }K_CS
Ticket Caching is not performed, so only weak authentication is provided. It is rumoured that implementations do not perform ticket caching.
Agents involved: Client, Authentication Server (AS), Ticket Granting server
(TGS), Server where the client needs to authenticate (Server)
% Authentication Server
role kerberos_A (A, C, G : agent,
Snd, Rcv : channel (dy),
K_CA, K_AG : symmetric_key)
played_by A
def=
local St : nat,
K_CG : symmetric_key,
N1, Lifetime_1 : text,
Tstart, Texpire : text
const k_cg1, k_cg2 : protocol_id,
sec_a_K_CG : protocol_id
init St := 0
transition
1. St = 0 /\ Rcv(C.G.Lifetime_1'.N1') =|>
St':= 1 /\ Tstart' := new()
/\ Texpire' := new()
/\ K_CG' := new()
/\ Snd(C.{C.G.K_CG'.Tstart'.Texpire'}_K_AG.
{G.K_CG'.Tstart'.Texpire'.N1'}_K_CA)
/\ witness(A,C,k_cg1,K_CG')
/\ witness(A,G,k_cg2,K_CG')
/\ secret(K_CG',sec_a_K_CG,{A,C,G})
end role
% Ticket Granting Server
role kerberos_G (G, A, S, C : agent,
Snd, Rcv : channel (dy),
K_AG, K_GS : symmetric_key)
played_by G
def=
local St : nat,
K_CG : symmetric_key,
K_CS : symmetric_key,
Lifetime_2, Tstart, Texpire, T, N2 : text,
Tstart2, Texpire2 : text
const t1, k_cs1, k_cs2 : protocol_id,
sec_g_K_CG, sec_g_K_CS : protocol_id
init St := 0
transition
1. St = 0 /\
Rcv(S.Lifetime_2'.N2'.{C.G.K_CG'.Tstart'.Texpire'}_K_AG.{C.T'}_K_CG') =|>
St':= 1 /\ K_CS' := new()
/\ Tstart2' := new()
/\ Texpire2' := new()
/\ Snd(C.
{C.S.K_CS'.Tstart2'.Texpire2'}_K_GS.
{S.K_CS'.Tstart2'.Texpire2'.N2'}_K_CG')
/\ wrequest(G,C,t1,T')
/\ wrequest(G,A,k_cg2,K_CG')
/\ witness(G,C,k_cs1,K_CS')
/\ witness(G,S,k_cs2,K_CS')
/\ secret(K_CG',sec_g_K_CG,{A,C,G})
/\ secret(K_CS',sec_g_K_CS,{G,C,S})
end role
% Server
role kerberos_S (S, G, C : agent,
Snd, Rcv : channel (dy),
K_GS : symmetric_key)
played_by S
def=
local St : nat,
Tstart2, Texpire2, T2 : text,
K_CS : symmetric_key
const t2a, t2b : protocol_id,
sec_s_K_CS : protocol_id
init St := 0
transition
1. St = 0 /\ Rcv({C.S.K_CS'.Tstart2'.Texpire2'}_K_GS.{C.T2'}_K_CS') =|>
St':= 1 /\ Snd({T2'}_K_CS')
/\ witness(S,C,t2a,T2')
/\ wrequest(S,G,k_cs2,K_CS')
/\ wrequest(S,C,t2b,T2')
/\ secret(K_CS',sec_s_K_CS,{G,C,S})
end role
% Client
role kerberos_C (C, A, G, S : agent,
Snd, Rcv : channel (dy),
K_CA : symmetric_key)
played_by C
def=
local St : nat,
K_CG, K_CS : symmetric_key,
T, T2 : text,
Tstart, Texpire, Tstart2, Texpire2 : text,
Ticket_1, Ticket_2 : {agent.agent.symmetric_key.text.text}_symmetric_key,
N1, N2 : text
const sec_c_K_CG, sec_c_K_CS : protocol_id,
cLifetime_1, cLifetime_2: text
init St := 0
transition
1. St = 0 /\ Rcv(start) =|>
St':= 1 /\ N1' := new()
/\ Snd(C.G.cLifetime_1.N1')
2. St = 1 /\ Rcv(C.Ticket_1'.{G.K_CG'.Tstart'.Texpire'.N1}_K_CA) =|>
St':= 2 /\ N2' := new()
/\ T' := new()
/\ Snd(S.cLifetime_2.N2'.Ticket_1'.{C.T'}_K_CG')
/\ witness(C,G,t1,T')
/\ wrequest(C,A,k_cg1,K_CG')
/\ secret(K_CG',sec_c_K_CG,{A,C,G})
3. St = 2 /\ Rcv(C.Ticket_2'.{S.K_CS'.Tstart2'.Texpire2'.N2}_K_CG) =|>
St':= 3 /\ T2' := new()
/\ Snd(Ticket_2'.{C.T2'}_K_CS')
/\ witness(C,S,t2b,T2')
/\ wrequest(C,G,k_cs1,K_CS')
/\ secret(K_CS',sec_c_K_CS,{G,C,S})
4. St = 3 /\ Rcv({T2}_K_CS) =|>
St':= 4 /\ wrequest(C,S,t2a,T2)
end role
role session( C, A, G, S : agent,
K_CA, K_AG, K_GS : symmetric_key)
def=
local S_C, R_C, S_A, R_A, S_G, R_G, S_S, R_S : channel (dy)
composition
kerberos_C(C,A,G,S,S_C,R_C,K_CA)
/\ kerberos_A(A,C,G,S_A,R_A,K_CA,K_AG)
/\ kerberos_G(G,A,S,C,S_G,R_G,K_AG,K_GS)
/\ kerberos_S(S,G,C,S_S,R_S,K_GS)
end role
role environment() def=
const c, a, g, s, i : agent,
kca, kag, kgs, kia : symmetric_key
intruder_knowledge = {c,a,g,s,kia
}
composition
session(c,a,g,s,kca,kag,kgs)
/\ session(i,a,g,s,kia,kag,kgs)
end role
goal
%secrecy_of K_CG, K_CS
secrecy_of sec_a_K_CG,
sec_g_K_CG, sec_g_K_CS,
sec_s_K_CS,
sec_c_K_CG, sec_c_K_CS % addresses G10
%Kerberos_C weakly authenticates Kerberos_A on k_cg
weak_authentication_on k_cg1 % addresses G1, G7, and G8
%Kerberos_G weakly authenticates Kerberos_A on k_cg
weak_authentication_on k_cg2 % addresses G1, G7, and G8
%Kerberos_C weakly authenticates Kerberos_G on k_cs
weak_authentication_on k_cs1 % addresses G1, G7, and G8
%Kerberos_S weakly authenticates Kerberos_G on k_cs
weak_authentication_on k_cs2 % addresses G1, G7, and G8
%Kerberos_C weakly authenticates Kerberos_S on t2a
weak_authentication_on t2a % addresses G1 and G2
%Kerberos_S weakly authenticates Kerberos_C on t2b
weak_authentication_on t2b % addresses G1 and G2
%Kerberos_G weakly authenticates Kerberos_C on t1
weak_authentication_on t1 % addresses G1 and G2
end goal
environment()