Abstract
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 constraint-based analysis techniques.
Original language | Undefined |
---|---|
Title of host publication | IEEE Symposium on Security and Privacy |
Place of Publication | Los Alamitos, California |
Publisher | IEEE Computer Society |
Pages | 155-168 |
Number of pages | 15 |
ISBN (Print) | 0-7695-2574-1 |
DOIs | |
Publication status | Published - Jan 2006 |
Event | 27th IEEE Symposium on Security and Privacy 2006 - The Claremont Resort , Oakland, United States Duration: 21 May 2006 → 25 May 2006 Conference number: 27 http://www.ieee-security.org/TC/SP2006/oakland06.html |
Publication series
Name | |
---|---|
Publisher | IEEE Computer Society |
Conference
Conference | 27th IEEE Symposium on Security and Privacy 2006 |
---|---|
Country/Territory | United States |
City | Oakland |
Period | 21/05/06 → 25/05/06 |
Internet address |
Keywords
- SCS-Cybersecurity
- IR-65549
- METIS-237429
- EWI-1791