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

• Protocol: set of traces

• 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

Any message

Destination agent

ACTUAL source agent!

Previous slide

Next slide

Back to first slide

View graphic version