A Trace Logic for Local Security Properties

Ricardo Corin, Antonio Durante, Sandro Etalle, Pieter Hartel

    Research output: Book/ReportReportOther research output

    33 Downloads (Pure)

    Abstract

    We propose a new simple trace logic that can be used to specify local security properties, i.e. security properties that refer to a single participant of the protocol specication. Our technique allows a protocol designer to provide formal specication of the desired security properties, and integrate them naturally to the design process of cryptographic protocols. Furthermore, the logic can be used for formal verication. We illustrate the utility of our technique by exposing new attacks on the well studied protocol TMN.
    Original languageEnglish
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages11
    Publication statusPublished - Apr 2003

    Publication series

    NameCTIT technical reports series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
    No.TR-CTIT-03-21

    Keywords

    • EC Grant Agreement nr.: FP5/34734
    • SCS-Cybersecurity

    Cite this

    Corin, R., Durante, A., Etalle, S., & Hartel, P. (2003). A Trace Logic for Local Security Properties. (CTIT technical reports series; No. TR-CTIT-03-21). Enschede: Centre for Telematics and Information Technology (CTIT).