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 language | English |
|---|---|
| Title of host publication | Proceedings of the International Workshop on Software Verification and Validation (SVV 2003) |
| Editors | S. Etalle, S. Mukhopadhyay, A. Roychoudhury |
| Place of Publication | Amsterdam |
| Publisher | Elsevier |
| Pages | 129-143 |
| Number of pages | 15 |
| DOIs | |
| Publication status | Published - Dec 2003 |
| Event | International Workshop on Software Verification and Validation, SVV 2003 - Mumbai, India Duration: 14 Dec 2003 → 14 Dec 2003 |
Publication series
| Name | Electronic Notes in Theoretical Computer Science |
|---|---|
| Publisher | Elsevier |
| Volume | 118 |
| ISSN (Print) | 1571-0661 |
Conference
| Conference | International Workshop on Software Verification and Validation, SVV 2003 |
|---|---|
| Abbreviated title | SVV |
| Country | India |
| City | Mumbai |
| Period | 14/12/03 → 14/12/03 |
Fingerprint
Keywords
- EC Grant Agreement nr.: FP5/34734
- SCS-Cybersecurity
- Trace logic
- Local security property
- Specification
- TMN protocol
Cite this
Corin, R., Durante, A., & Hartel, P. (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). Amsterdam: Elsevier. https://doi.org/10.1016/j.entcs.2004.12.019