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: Proceedings of the International Workshop on Software Verification and Validation (SVV 2003). Electronic Notes in Theoretical Computer Science, 118 (1). Elsevier, pp. 129-143.

Preview

PDF
156Kb

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
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Distributed and Embedded Systems (DIES)
Link to this item:	http://purl.utwente.nl/publications/41376
Official URL:	http://dx.doi.org/10.1016/j.entcs.2004.12.019
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 214060