An intruder model for verifying liveness in security protocols

J.G. Cederquist, Muhammad Torabi Dashti

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    11 Citations (Scopus)


    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.
    Original languageUndefined
    Title of host publicationFMSE '06: Proceedings of the fourth ACM workshop on Formal methods in security
    Place of PublicationNew York
    PublisherAssociation for Computing Machinery (ACM)
    Number of pages10
    ISBN (Print)1-59593-550-9
    Publication statusPublished - 2006
    EventFourth ACM Workshop on Formal Methods in Security, FMSE '06 - Alexandria, Virginia, USA
    Duration: 3 Nov 20063 Nov 2006

    Publication series



    WorkshopFourth ACM Workshop on Formal Methods in Security, FMSE '06
    OtherNovember 3, 2006


    • SCS-Cybersecurity
    • EWI-9140
    • METIS-237420
    • IR-63933

    Cite this