The Dolev-Yao attacker (/ intruder) model is a standard list of strong assumptions about an attacker, which protocols shown secure in respect to means they would work in a large range of environments:

  • Attacker can intercept and read all messages
  • Attacker can decompose messages into their parts (cryptography is secure and decryption requires inverse keys)
  • Attacker can build new messages with different constructors
  • Attacker can send messages at any time