A Trace Logic for Local Security Properties

Ricardo Corin, Antonio Durante, Pieter Hartel

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

    21 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 specification. Our technique allows a protocol designer to provide a formal specification of the desired security properties, and integrate it naturally into the design process of cryptographic protocols. Furthermore, the logic can be used for formal verification. We illustrate the utility of our technique by exposing new attacks on the well studied TMN protocol.
    Original languageEnglish
    Title of host publicationProceedings of the International Workshop on Software Verification and Validation (SVV 2003)
    EditorsS. Etalle, S. Mukhopadhyay, A. Roychoudhury
    Place of PublicationAmsterdam
    PublisherElsevier
    Pages129-143
    Number of pages15
    DOIs
    Publication statusPublished - Dec 2003
    EventInternational Workshop on Software Verification and Validation, SVV 2003 - Mumbai, India
    Duration: 14 Dec 200314 Dec 2003

    Publication series

    NameElectronic Notes in Theoretical Computer Science
    PublisherElsevier
    Volume118
    ISSN (Print)1571-0661

    Conference

    ConferenceInternational Workshop on Software Verification and Validation, SVV 2003
    Abbreviated titleSVV
    CountryIndia
    CityMumbai
    Period14/12/0314/12/03

    Keywords

    • EC Grant Agreement nr.: FP5/34734
    • SCS-Cybersecurity
    • Trace logic
    • Local security property
    • Specification
    • TMN protocol

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

    Cite this