Interrogator, cont’d

• Attacker’s transition: replace MsgOut by a MsgIn created by the attacker from known message fields

• A message field X is known by the attacker if:

  • It has appeared unencrypted in a prior message
  • It has appeared encrypted in a key known to the attacker
  • Expressed as Prolog predicate

    pKnows(X, MsgHistory, State) defined recursively
    

• Encryption operator rules were built in

  • Xor, exponentiation were included

Previous slide

Next slide

Back to first slide

View graphic version