-- Otway Rees Protocol
-- Script used in the book

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

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


#Protocol description
0.    -> a : b
[a != b]
1a. a -> b : a, b, m
[a != b]
1b. a -> s : {na, m, a, b}{ServerKey(a)} 
2.  b -> s : m, a, b, {nb, m, a, b}{ServerKey(b)}
3.  s -> b : m, {nb, kab}{ServerKey(b)}
4.  s -> a : m, {na, kab}{ServerKey(a)}

#Specification
Secret(a,kab,[b,s])
StrongSecret(a,kab,[b,s])
Secret(b,kab,[a,s])
Agreement(a,b,[m])
Agreement(b,a,[m])

#Actual variables
Alice, Bob, Ivo : Agent
Sam : Server
Na, Nb, Nm, M : Nonce
Kab1, Kab2 : SessionKey
InverseKeys = (Kab1, Kab1), (Kab2, Kab2)

#Functions
symbolic ServerKey

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


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