A Trace Logic for Local Security Properties


Corin, Ricardo and Durante, Antonio and Etalle, Sandro and Hartel, Pieter (2005) 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, 118 (1). Elsevier, pp. 129-143.

open access
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.
Item Type:Book Section
Copyright:© 2005 Elsevier
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/41376
Official URL:https://doi.org/10.1016/j.entcs.2004.12.019
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 214060