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

30 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