#Free variables
a, b : Agent
s : Server
na, nb : Nonce
kab : SessionKey
ServerKey : Agent -> ServerKeys
InverseKeys = (kab, kab), (ServerKey, ServerKey)

#Processes
INITIATOR(a,na) knows ServerKey(a)
RESPONDER(b,s,nb) knows ServerKey(b)
SERVER(s,kab) knows ServerKey

#Protocol description
0.    -> a : b
1.  a -> b : na
2.  b -> s : {a, na, nb}{ServerKey(b)}
3 . s -> a : {b, kab, na, nb}{ServerKey(a)}, {a, kab}{ServerKey(b)} % v
4.  a -> b : v % {a, kab}{ServerKey(b)}, {nb}{kab}

#Specification
Secret(a, kab, [b,s])
Secret(b, kab, [a,s])
Agreement(b, a, [na,nb])
Agreement(a, b, [kab])

#Actual variables
Alice, Bob, Ivo : Agent
Sam : Server
Kab : SessionKey
Na, Nb : Nonce
InverseKeys = (Kab, Kab)

#Inline functions
symbolic ServerKey

#System
INITIATOR(Alice, Na)
RESPONDER(Bob, Sam, Nb)
SERVER(Sam, Kab)

#Intruder Information
Intruder = Ivo
IntruderKnowledge = {Alice, Bob, Ivo, Sam, ServerKey(Ivo)}