Sciweavers

Share
CCS
2006
ACM

An intruder model for verifying liveness in security protocols

9 years 7 months ago
An intruder model for verifying liveness in security protocols
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.
Jan Cederquist, Muhammad Torabi Dashti
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where CCS
Authors Jan Cederquist, Muhammad Torabi Dashti
Comments (0)
books