Timed Model Checking of Security Protocols

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

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

    162 Downloads (Pure)

    Abstract

    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
    Title of host publication2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE)
    EditorsV. Atluri, M. Backes, D.A. Basin, M. Waidner
    Place of PublicationNew York
    PublisherACM Press
    Pages23-32
    Number of pages10
    ISBN (Print)1-58113-971-3
    DOIs
    Publication statusPublished - Oct 2004
    Event2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE) - Fairfax, Virginia
    Duration: 1 Oct 20041 Oct 2004

    Publication series

    Name
    PublisherACM Press

    Workshop

    Workshop2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE)
    Period1/10/041/10/04

    Keywords

    • EWI-766
    • IR-48643
    • METIS-220303
    • SCS-Cybersecurity

    Cite this