-- Needham Schroeder Public Key Protocol, 7 message version.

#Free variables
a, b : Agent
s: Server
na, nb : Nonce
pka, pkb : PublicKey
PK : Agent -> PublicKey
SK : Agent -> SecretKey
SPK : Server -> ServerPublicKey
SSK : Server -> ServerSecretKey
InverseKeys = (PK,SK), (SPK, SSK)

#Processes
INITIATOR(a,s,na) knows SK(a), SPK
RESPONDER(b,s,nb) knows SK(b), SPK
SERVER(s) knows PK, SSK

#Protocol description
0.    -> a : b
-- [a != b]
1.  a -> s : b  
2.  s -> a : {b, PK(b) % pkb}{SSK(s)}
3.  a -> b : {na, a}{pkb % PK(b)}
4.  b -> s : a
5.  s -> b : {a, PK(a) % pka}{SSK(s)}
6.  b -> a : {na, nb}{pka % PK(a)}
7.  a -> b : {nb}{pkb % PK(b)}

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

#Actual variables
Alice, Bob, Ivo : Agent
Sam : Server
Na, Nb, Nm : Nonce

#Inline functions

symbolic PK, SK, SPK, SSK

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

#Intruder Information
Intruder = Ivo
IntruderKnowledge = {Alice, Bob, Ivo, Nm, Sam, PK, SPK, SK(Ivo)}