-- Otway Rees Protocol
-- Script used in the book, without redirecting

#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]
1. a -> b : a, b, m, {na, m, a, b}{ServerKey(a)} % v
[a != b]
2a. b -> s : m, a, b, v % {na, m, a, b}{ServerKey(a)} 
2b. b -> s : {nb, m, a, b}{ServerKey(b)}
3a. s -> b : m, {na, kab}{ServerKey(a)} % w
3b. s -> b : {nb, kab}{ServerKey(b)}
4. b -> a : m, w % {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, M : Nonce
Kab1 : 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, M, ServerKey(Ivo)}