An intruder model for verifying liveness in security protocols

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.

PDF
Restricted to UT campus only: Request a copy
225Kb

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:	Distributed and Embedded Systems (DIES)
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

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 237420