Paulson’s Modeling Approach
Primitive message field types: Agent, Key, Nonce
Constructed message fields: {X, Y}, Crypt K X
Message event: Says A B X
Trace: sequence of message events
Transition - based protocol definition of protocol P :
- Recursive: Let T be a trace in P, then
- (Says Spy B M) may be appended if M in synth(analz(set(T)))
- (Says A B M) may be appended by a protocol rule