Timed Model Checking of Security Protocols

R.J. Corin, Sandro Etalle, Pieter H. Hartel, Angelika H. Mader

    Research output: Book/ReportReportOther research output

    35 Citations (Scopus)
    169 Downloads (Pure)


    We propose a method for engineering security protocols that are aware of timing aspects. We study a simplified version of the well-known Needham Schroeder protocol and the complete Yahalom protocol. Timing information allows the study of different attack scenarios. We illustrate the attacks by model checking the protocol using Uppaal. We also present new challenges and threats that arise when considering time.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages355
    Publication statusPublished - Jun 2004

    Publication series

    NameCTIT technical report series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)


    • EWI-6047
    • SCS-Cybersecurity
    • IR-56999

    Cite this