A Logic for Constraint-based Security Protocol Analysis

We propose PS-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 constraintbased analysis techniques.

• Type: Conference
• Year: 2006
• Where: SP
• Authors: Ricardo Corin, Sandro Etalle, Ari Saptawijaya
• Keywords: Data Freshness Properties, Linear Temporal Logic, Security Privacy, SP 2006, Symbolic Execution Traces