An Intruder Model for Verifying Termination in Security Protocols

J.G. Cederquist, M.T. Dashti

    Research output: Book/ReportReportProfessional

    88 Downloads (Pure)


    We formally describe an intruder that is suitable for checking fairness properties of security protocols. The intruder is proved to be equivalent to the Dolev-Yao intruder that respects the resilient communication channels assumption, in the sense that, if a fairness property holds in one of these models, it also holds in the other.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages13
    Publication statusPublished - Jul 2005

    Publication series

    NameCTIT Technical Report Series
    ISSN (Print)1381-3625


    • IR-54532
    • METIS-228788
    • SCS-Cybersecurity
    • EWI-723

    Cite this