We present a process algebraic intruder model for verifying a class of liveness properties of security protocols. For this class, the proposed intruder model is proved to be equivalent to a Dolev-Yao intruder that does not delay indefinitely the delivery of messages. In order to prove the equivalence, we formalize the resilient communication channels assumption. As an application of the proposed intruder model, formal verification of fair exchange protocols is discussed.
|Title of host publication||FMSE '06: Proceedings of the fourth ACM workshop on Formal methods in security|
|Place of Publication||New York|
|Publisher||Association for Computing Machinery (ACM)|
|Number of pages||10|
|Publication status||Published - 2006|
Cederquist, J. G., & Dashti, M. T. (2006). An intruder model for verifying liveness in security protocols. In FMSE '06: Proceedings of the fourth ACM workshop on Formal methods in security (pp. 23-32). [10.1145/1180337.1180340] New York: Association for Computing Machinery (ACM). https://doi.org/10.1145/1180337.1180340