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 specication. Our technique allows a protocol designer to provide formal specication of the desired security properties, and integrate them naturally to the design process of cryptographic protocols. Furthermore, the logic can be used for formal verication. We illustrate the utility of our technique by exposing new attacks on the well studied protocol TMN.
|Name||CTIT technical reports series|
|Publisher||University of Twente, Centre for Telematics and Information Technology (CTIT)|
- EC Grant Agreement nr.: FP5/34734