Dolev-Yao, cont’d
Strong attacker and strong encryption assumptions
- Attacker intercepts every message
- Attacker can cause an party to apply any of its operators at any time (by starting new sessions)
- Attacker can apply any operator except other’s decryption
Results:
- Security decidable in polynomial time for this class
- Security undecidable for a more general (two-field) models [EG83, HT96]
- Moral: analysis is difficult because attacker can exploit interactions between two or more sessions