protocol DenningSacco;
identifiers
A,B,S       :user;
Kas,Kbs,T       :number;
Kab     :symmetric_key;

messages
1. A -> S: A, B
2. S -> A: {B, Kab, T, {Kab, A, T}Kbs}Kas
3. A -> B: {Kab, A, T}Kbs

knowledge
A   : A, B, S, Kas;
B   : A, B, S, Kbs;
S   : A, B, S, Kab, Kas, Kbs, T;

session_instances
 [A:alice,B:bob,S:server,Kas:kas,Kbs:kbs,T:t]
 [A:i,B:bob,S:server,Kas:kis,Kbs:kbs,T:t]
;
intruder_knowledge
 bob,server,kis;

goal
 secrecy_of Kab [A,B];