An intruder model for verifying liveness in security protocols


Share/Save/Bookmark

Cederquist, Jan and Dashti, Muhammad Torabi (2006) An intruder model for verifying liveness in security protocols. In: Fourth ACM Workshop on Formal Methods in Security, FMSE '06, November 3, 2006, Alexandria, Virginia, USA (pp. pp. 23-32).

[img] PDF
Restricted to UT campus only
: Request a copy
231kB
Abstract: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.
Item Type:Conference or Workshop Item
Copyright:© 2006 ACM
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/63933
Official URL:http://doi.acm.org/10.1145/1180337.1180340
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 237420