-- Needham Schroeder Signature Protocol
#Free variables
a, b : Agent
s : Server
m : Text
SKey : Agent -> ServerKey
f : HashFunction
InverseKeys = (SKey, SKey)

#Processes
INITIATOR(a, s, m) knows SKey(a)
RESPONDER(b, s) knows SKey(b)
SERVER(s) knows SKey

#Protocol description
0.   -> a : b
1. a -> b : m
2. a -> s : b, {f(m) % cs}{SKey(a)}
3. s -> b : {a, cs % f(m)}{SKey(b)}

#Specification
Agreement(a, b, [m])
Aliveness(a,b)

#Actual variables
Alice, Bob, Mallory : Agent
Sam : Server
M : Text

#Functions
symbolic SKey

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

#Intruder Information

Intruder = Mallory
IntruderKnowledge = {Alice, Bob, Mallory, Sam, SKey(Mallory)}