Title :
A logic for constraint-based security protocol analysis
Author :
Corin, R. ; Saptawijaya, A.
Author_Institution :
Twente Univ.
Abstract :
We propose VS-LTL, a pure-past security linear temporal logic that allows the specification of a variety of authentication, secrecy and data freshness properties. Furthermore, we present a sound and complete decision procedure to establish the validity of security properties for symbolic execution traces, and show the integration with constraint-based analysis techniques
Keywords :
authorisation; constraint handling; formal specification; temporal logic; VS-LTL; authentication specification; constraint-based security protocol analysis; data freshness; pure-past security linear temporal logic; secrecy specification; symbolic execution traces; Access protocols; Authentication; Communication system control; Computer crime; Cryptographic protocols; Cryptography; Data security; Internet; Logic; Testing;
Conference_Titel :
Security and Privacy, 2006 IEEE Symposium on
Conference_Location :
Berkeley/Oakland, CA
Print_ISBN :
0-7695-2574-1
