A Logic for Constraint-based Security Protocol Analysis

R.J. Corin; A. Saptawijaya; Sandro Etalle

doi:10.1109/SP.2006.3

A Logic for Constraint-based Security Protocol Analysis

R.J. Corin, A. Saptawijaya, Sandro Etalle

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

31 Citations (Scopus)

89 Downloads (Pure)

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	https://doi.org/10.1109/SP.2006.3
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	United States
City	Oakland
Period	21/05/06 → 25/05/06
Internet address	http://www.ieee-security.org/TC/SP2006/oakland06.html

Keywords

SCS-Cybersecurity
IR-65549
METIS-237429
EWI-1791

Access to Document

10.1109/SP.2006.3

corin-logic
open
corin-logic
open

Cite this

@inproceedings{9d49a89cbc1e41abad59b724f6f7a7fe,

title = "A Logic for Constraint-based Security Protocol Analysis",

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.",

keywords = "SCS-Cybersecurity, IR-65549, METIS-237429, EWI-1791",

author = "R.J. Corin and A. Saptawijaya and Sandro Etalle",

note = "10.1109/SP.2006.3 ; null ; Conference date: 21-05-2006 Through 25-05-2006",

year = "2006",

month = jan,

doi = "10.1109/SP.2006.3",

language = "Undefined",

isbn = "0-7695-2574-1",

publisher = "IEEE Computer Society",

pages = "155--168",

booktitle = "IEEE Symposium on Security and Privacy",

address = "United States",

url = "http://www.ieee-security.org/TC/SP2006/oakland06.html",

}

TY - GEN

T1 - A Logic for Constraint-based Security Protocol Analysis

AU - Corin, R.J.

AU - Saptawijaya, A.

AU - Etalle, Sandro

N1 - Conference code: 27

PY - 2006/1

Y1 - 2006/1

N2 - 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.

AB - 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.

KW - SCS-Cybersecurity

KW - IR-65549

KW - METIS-237429

KW - EWI-1791

U2 - 10.1109/SP.2006.3

DO - 10.1109/SP.2006.3

M3 - Conference contribution

SN - 0-7695-2574-1

SP - 155

EP - 168

BT - IEEE Symposium on Security and Privacy

PB - IEEE Computer Society

CY - Los Alamitos, California

Y2 - 21 May 2006 through 25 May 2006

ER -