A Trace Logic for Local Security Properties

R.J. Corin, Antonio Durante, Pieter H. Hartel

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

    34 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 languageUndefined
    Title of host publicationProceedings of the International Workshop on Software Verification and Validation (SVV 2003)
    EditorsSandro 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
    Number1
    Volume118
    ISSN (Print)1571-0661
    ISSN (Electronic)1571-0661

    Conference

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

    Keywords

    • IR-41376
    • EC Grant Agreement nr.: FP5/34734
    • METIS-214060
    • SCS-Cybersecurity
    • EWI-822

    Cite this

    Corin, R. J., Durante, A., & Hartel, P. H. (2003). A Trace Logic for Local Security Properties. In S. Etalle, S. Mukhopadhyay, & A. Roychoudhury (Eds.), Proceedings of the International Workshop on Software Verification and Validation (SVV 2003) (pp. 129-143). (Electronic Notes in Theoretical Computer Science; Vol. 118, No. 1). Amsterdam: Elsevier. https://doi.org/10.1016/j.entcs.2004.12.019
    Corin, R.J. ; Durante, Antonio ; Hartel, Pieter H. / A Trace Logic for Local Security Properties. Proceedings of the International Workshop on Software Verification and Validation (SVV 2003). editor / Sandro Etalle ; S. Mukhopadhyay ; A. Roychoudhury. Amsterdam : Elsevier, 2003. pp. 129-143 (Electronic Notes in Theoretical Computer Science; 1).
    @inproceedings{59b58ccb001c40dc84eda2267037ece3,
    title = "A Trace Logic for Local Security Properties",
    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.",
    keywords = "IR-41376, EC Grant Agreement nr.: FP5/34734, METIS-214060, SCS-Cybersecurity, EWI-822",
    author = "R.J. Corin and Antonio Durante and Hartel, {Pieter H.}",
    note = "Imported from DIES",
    year = "2003",
    month = "12",
    doi = "10.1016/j.entcs.2004.12.019",
    language = "Undefined",
    series = "Electronic Notes in Theoretical Computer Science",
    publisher = "Elsevier",
    number = "1",
    pages = "129--143",
    editor = "Sandro Etalle and S. Mukhopadhyay and A. Roychoudhury",
    booktitle = "Proceedings of the International Workshop on Software Verification and Validation (SVV 2003)",

    }

    Corin, RJ, Durante, A & Hartel, PH 2003, A Trace Logic for Local Security Properties. in S Etalle, S Mukhopadhyay & A Roychoudhury (eds), Proceedings of the International Workshop on Software Verification and Validation (SVV 2003). Electronic Notes in Theoretical Computer Science, no. 1, vol. 118, Elsevier, Amsterdam, pp. 129-143, International Workshop on Software Verification and Validation, Mumbai, India, 14/12/03. https://doi.org/10.1016/j.entcs.2004.12.019

    A Trace Logic for Local Security Properties. / Corin, R.J.; Durante, Antonio; Hartel, Pieter H.

    Proceedings of the International Workshop on Software Verification and Validation (SVV 2003). ed. / Sandro Etalle; S. Mukhopadhyay; A. Roychoudhury. Amsterdam : Elsevier, 2003. p. 129-143 (Electronic Notes in Theoretical Computer Science; Vol. 118, No. 1).

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

    TY - GEN

    T1 - A Trace Logic for Local Security Properties

    AU - Corin, R.J.

    AU - Durante, Antonio

    AU - Hartel, Pieter H.

    N1 - Imported from DIES

    PY - 2003/12

    Y1 - 2003/12

    N2 - 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.

    AB - 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.

    KW - IR-41376

    KW - EC Grant Agreement nr.: FP5/34734

    KW - METIS-214060

    KW - SCS-Cybersecurity

    KW - EWI-822

    U2 - 10.1016/j.entcs.2004.12.019

    DO - 10.1016/j.entcs.2004.12.019

    M3 - Conference contribution

    T3 - Electronic Notes in Theoretical Computer Science

    SP - 129

    EP - 143

    BT - Proceedings of the International Workshop on Software Verification and Validation (SVV 2003)

    A2 - Etalle, Sandro

    A2 - Mukhopadhyay, S.

    A2 - Roychoudhury, A.

    PB - Elsevier

    CY - Amsterdam

    ER -

    Corin RJ, Durante A, Hartel PH. A Trace Logic for Local Security Properties. In Etalle S, Mukhopadhyay S, Roychoudhury A, editors, Proceedings of the International Workshop on Software Verification and Validation (SVV 2003). Amsterdam: Elsevier. 2003. p. 129-143. (Electronic Notes in Theoretical Computer Science; 1). https://doi.org/10.1016/j.entcs.2004.12.019