An intruder model for verifying termination in security protocols
Jan Cederquist, Mohammad Torabi Dashti · University of Twente Research Information · 2005
We formally describe an intruder that is suitable for checking fairness properties of security protocols. The intruder is proved to be equivalent to the Dolev-Yao intruder that respects the resilient communication channels assumption, in the sense that, if a fairness property holds in one of these models, it also holds in the other.