A Trace Logic for Local Security Properties

Ricardo Corin, Antonio Durante, Sandro Etalle, Pieter Hartel

    Research output: Book/ReportReportOther research output

    84 Downloads (Pure)


    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)


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


    Dive into the research topics of 'A Trace Logic for Local Security Properties'. Together they form a unique fingerprint.

    Cite this