PS-LTL for Constraint-Based Security Protocol Analysis

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

Several formal approaches have been proposed to analyse security protocols, e.g. [2,7,11,1,6,12]. Recently, a great interest has been growing on the use of constraint solving approach. Initially proposed by Millen and Shmatikov [9], this approach allows analysis of a finite number of protocol sessions. Yet, the representation of protocol runs by symbolic traces (as opposed to concrete traces) captures the possibility of having unbounded message space, allowing analysis over an infinite state space. A constraint is defined as a pair consisting of a message M and a set of messages K that represents the intruder¿s knowledge. Millen and Shmatikov present a procedure to solve a set of constraints, i.e. that in each constraint, M can be built from K. When a set of constraints is solved, then a concrete trace representing an attack over the protocol can be extracted. Corin and Etalle [4] has improved the work of Millen and Shmatikov by presenting a more efficient procedure. However, none of these constraint-based systems provide enough flexibility and expresiveness in specifying security properties. For example, to check secrecy an artificial protocol role is added to simulate whether a secret can be learned by an intruder. Authentication cannot also be checked directly. Moreover, only a built-in notion of authentication is implemented by Millen and Shmatikov in his Prolog implementation [10]. This problem motivates our current work. A logical formalism is considered to be an appropriate solution to improve the flexibility and expresiveness in specifying security properties. A preliminary attempt to use logic for specifying local security properties in a constraint-based setting has been carried out [3]. Inspired by this work and the successful NPATRL [11,8], we currently explores a variant of linear temporal logic (LTL) over finite traces, -LTL, standing for pure-past security LTL [5]. In contrast to standard LTL, this logic deals only with past events in a trace. In our current work, a protocol is modelled as in previous works [9,4,3], viz. by protocol roles. A protocol role is a sequence of send and receive events, together with status events to indicate, e.g. that a protocol role has completed her protocol run. A scenario is then used to deal with the number of sessions and protocol roles considered in the analysis. Integrating -LTL into our constraint solving approach presents a challenge, since we need to develop a sound and complete decision procedure against symbolic traces, instead of concrete traces. Our idea to address this problem is by concretizing symbolic traces incrementally while deciding a formula. Basically, the decision procedure consists of two steps: transform and decide. The former step transforms a -LTL formula with respect to the current trace into a so-called elementary formula that is built from constraints and equalities using logical connectives and quantifiers. The decision is then performed by the latter step through solving the constraints and checking the equalities. Although we define a decision procedure for a fragment of -LTL, this fragment is expressive enough to specify several security properties, like various notions of secrecy and authentication, and also data freshness. We provide a Prolog implementation and have analysed several security protocols. There are many directions for improvement. From the implementation point of view, the efficiency of the decision procedure can still be improved. I would also like to investigate the expressiveness of the logic for speficying other security properties. This may result in an extension of the decision procedure for a larger fragment of the logic. Another direction is to characterize the expressivity power of -LTL compared to other security requirement languages.
Original languageUndefined
Title of host publicationLogic Programming, 21st International Conference, ICLP 2005
EditorsM. Gabbrielli, G. Gupta
Place of PublicationBerlin
PublisherSpringer
Pages439-440
Number of pages2
ISBN (Print)3-540-29208-X
DOIs
Publication statusPublished - Oct 2005
Event21st International Conference on Logic Programming, ICLP 2005 - Sitges, Spain
Duration: 2 Oct 20055 Oct 2005
Conference number: 21

Publication series

NameElectronic Notes in Theoretical Computer Science
PublisherSpringer Verlag
NumberRFC 4080
Volume3668
ISSN (Print)0302-9743

Conference

Conference21st International Conference on Logic Programming, ICLP 2005
Abbreviated titleICLP
CountrySpain
CitySitges
Period2/10/055/10/05

Keywords

  • SCS-Cybersecurity
  • IR-54523
  • METIS-248138
  • EWI-8040

Cite this

Corin, R. J., Saptawijaya, A., & Etalle, S. (2005). PS-LTL for Constraint-Based Security Protocol Analysis. In M. Gabbrielli, & G. Gupta (Eds.), Logic Programming, 21st International Conference, ICLP 2005 (pp. 439-440). (Electronic Notes in Theoretical Computer Science; Vol. 3668, No. RFC 4080). Berlin: Springer. https://doi.org/10.1007/11562931, https://doi.org/10.1007/11562931_46
Corin, R.J. ; Saptawijaya, A. ; Etalle, Sandro. / PS-LTL for Constraint-Based Security Protocol Analysis. Logic Programming, 21st International Conference, ICLP 2005. editor / M. Gabbrielli ; G. Gupta. Berlin : Springer, 2005. pp. 439-440 (Electronic Notes in Theoretical Computer Science; RFC 4080).
@inproceedings{e282b3a9ce544ef0afd2149e86b2ebd5,
title = "PS-LTL for Constraint-Based Security Protocol Analysis",
abstract = "Several formal approaches have been proposed to analyse security protocols, e.g. [2,7,11,1,6,12]. Recently, a great interest has been growing on the use of constraint solving approach. Initially proposed by Millen and Shmatikov [9], this approach allows analysis of a finite number of protocol sessions. Yet, the representation of protocol runs by symbolic traces (as opposed to concrete traces) captures the possibility of having unbounded message space, allowing analysis over an infinite state space. A constraint is defined as a pair consisting of a message M and a set of messages K that represents the intruder¿s knowledge. Millen and Shmatikov present a procedure to solve a set of constraints, i.e. that in each constraint, M can be built from K. When a set of constraints is solved, then a concrete trace representing an attack over the protocol can be extracted. Corin and Etalle [4] has improved the work of Millen and Shmatikov by presenting a more efficient procedure. However, none of these constraint-based systems provide enough flexibility and expresiveness in specifying security properties. For example, to check secrecy an artificial protocol role is added to simulate whether a secret can be learned by an intruder. Authentication cannot also be checked directly. Moreover, only a built-in notion of authentication is implemented by Millen and Shmatikov in his Prolog implementation [10]. This problem motivates our current work. A logical formalism is considered to be an appropriate solution to improve the flexibility and expresiveness in specifying security properties. A preliminary attempt to use logic for specifying local security properties in a constraint-based setting has been carried out [3]. Inspired by this work and the successful NPATRL [11,8], we currently explores a variant of linear temporal logic (LTL) over finite traces, -LTL, standing for pure-past security LTL [5]. In contrast to standard LTL, this logic deals only with past events in a trace. In our current work, a protocol is modelled as in previous works [9,4,3], viz. by protocol roles. A protocol role is a sequence of send and receive events, together with status events to indicate, e.g. that a protocol role has completed her protocol run. A scenario is then used to deal with the number of sessions and protocol roles considered in the analysis. Integrating -LTL into our constraint solving approach presents a challenge, since we need to develop a sound and complete decision procedure against symbolic traces, instead of concrete traces. Our idea to address this problem is by concretizing symbolic traces incrementally while deciding a formula. Basically, the decision procedure consists of two steps: transform and decide. The former step transforms a -LTL formula with respect to the current trace into a so-called elementary formula that is built from constraints and equalities using logical connectives and quantifiers. The decision is then performed by the latter step through solving the constraints and checking the equalities. Although we define a decision procedure for a fragment of -LTL, this fragment is expressive enough to specify several security properties, like various notions of secrecy and authentication, and also data freshness. We provide a Prolog implementation and have analysed several security protocols. There are many directions for improvement. From the implementation point of view, the efficiency of the decision procedure can still be improved. I would also like to investigate the expressiveness of the logic for speficying other security properties. This may result in an extension of the decision procedure for a larger fragment of the logic. Another direction is to characterize the expressivity power of -LTL compared to other security requirement languages.",
keywords = "SCS-Cybersecurity, IR-54523, METIS-248138, EWI-8040",
author = "R.J. Corin and A. Saptawijaya and Sandro Etalle",
note = "10.1007/11562931_46",
year = "2005",
month = "10",
doi = "10.1007/11562931",
language = "Undefined",
isbn = "3-540-29208-X",
series = "Electronic Notes in Theoretical Computer Science",
publisher = "Springer",
number = "RFC 4080",
pages = "439--440",
editor = "M. Gabbrielli and G. Gupta",
booktitle = "Logic Programming, 21st International Conference, ICLP 2005",

}

Corin, RJ, Saptawijaya, A & Etalle, S 2005, PS-LTL for Constraint-Based Security Protocol Analysis. in M Gabbrielli & G Gupta (eds), Logic Programming, 21st International Conference, ICLP 2005. Electronic Notes in Theoretical Computer Science, no. RFC 4080, vol. 3668, Springer, Berlin, pp. 439-440, 21st International Conference on Logic Programming, ICLP 2005, Sitges, Spain, 2/10/05. https://doi.org/10.1007/11562931, https://doi.org/10.1007/11562931_46

PS-LTL for Constraint-Based Security Protocol Analysis. / Corin, R.J.; Saptawijaya, A.; Etalle, Sandro.

Logic Programming, 21st International Conference, ICLP 2005. ed. / M. Gabbrielli; G. Gupta. Berlin : Springer, 2005. p. 439-440 (Electronic Notes in Theoretical Computer Science; Vol. 3668, No. RFC 4080).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - PS-LTL for Constraint-Based Security Protocol Analysis

AU - Corin, R.J.

AU - Saptawijaya, A.

AU - Etalle, Sandro

N1 - 10.1007/11562931_46

PY - 2005/10

Y1 - 2005/10

N2 - Several formal approaches have been proposed to analyse security protocols, e.g. [2,7,11,1,6,12]. Recently, a great interest has been growing on the use of constraint solving approach. Initially proposed by Millen and Shmatikov [9], this approach allows analysis of a finite number of protocol sessions. Yet, the representation of protocol runs by symbolic traces (as opposed to concrete traces) captures the possibility of having unbounded message space, allowing analysis over an infinite state space. A constraint is defined as a pair consisting of a message M and a set of messages K that represents the intruder¿s knowledge. Millen and Shmatikov present a procedure to solve a set of constraints, i.e. that in each constraint, M can be built from K. When a set of constraints is solved, then a concrete trace representing an attack over the protocol can be extracted. Corin and Etalle [4] has improved the work of Millen and Shmatikov by presenting a more efficient procedure. However, none of these constraint-based systems provide enough flexibility and expresiveness in specifying security properties. For example, to check secrecy an artificial protocol role is added to simulate whether a secret can be learned by an intruder. Authentication cannot also be checked directly. Moreover, only a built-in notion of authentication is implemented by Millen and Shmatikov in his Prolog implementation [10]. This problem motivates our current work. A logical formalism is considered to be an appropriate solution to improve the flexibility and expresiveness in specifying security properties. A preliminary attempt to use logic for specifying local security properties in a constraint-based setting has been carried out [3]. Inspired by this work and the successful NPATRL [11,8], we currently explores a variant of linear temporal logic (LTL) over finite traces, -LTL, standing for pure-past security LTL [5]. In contrast to standard LTL, this logic deals only with past events in a trace. In our current work, a protocol is modelled as in previous works [9,4,3], viz. by protocol roles. A protocol role is a sequence of send and receive events, together with status events to indicate, e.g. that a protocol role has completed her protocol run. A scenario is then used to deal with the number of sessions and protocol roles considered in the analysis. Integrating -LTL into our constraint solving approach presents a challenge, since we need to develop a sound and complete decision procedure against symbolic traces, instead of concrete traces. Our idea to address this problem is by concretizing symbolic traces incrementally while deciding a formula. Basically, the decision procedure consists of two steps: transform and decide. The former step transforms a -LTL formula with respect to the current trace into a so-called elementary formula that is built from constraints and equalities using logical connectives and quantifiers. The decision is then performed by the latter step through solving the constraints and checking the equalities. Although we define a decision procedure for a fragment of -LTL, this fragment is expressive enough to specify several security properties, like various notions of secrecy and authentication, and also data freshness. We provide a Prolog implementation and have analysed several security protocols. There are many directions for improvement. From the implementation point of view, the efficiency of the decision procedure can still be improved. I would also like to investigate the expressiveness of the logic for speficying other security properties. This may result in an extension of the decision procedure for a larger fragment of the logic. Another direction is to characterize the expressivity power of -LTL compared to other security requirement languages.

AB - Several formal approaches have been proposed to analyse security protocols, e.g. [2,7,11,1,6,12]. Recently, a great interest has been growing on the use of constraint solving approach. Initially proposed by Millen and Shmatikov [9], this approach allows analysis of a finite number of protocol sessions. Yet, the representation of protocol runs by symbolic traces (as opposed to concrete traces) captures the possibility of having unbounded message space, allowing analysis over an infinite state space. A constraint is defined as a pair consisting of a message M and a set of messages K that represents the intruder¿s knowledge. Millen and Shmatikov present a procedure to solve a set of constraints, i.e. that in each constraint, M can be built from K. When a set of constraints is solved, then a concrete trace representing an attack over the protocol can be extracted. Corin and Etalle [4] has improved the work of Millen and Shmatikov by presenting a more efficient procedure. However, none of these constraint-based systems provide enough flexibility and expresiveness in specifying security properties. For example, to check secrecy an artificial protocol role is added to simulate whether a secret can be learned by an intruder. Authentication cannot also be checked directly. Moreover, only a built-in notion of authentication is implemented by Millen and Shmatikov in his Prolog implementation [10]. This problem motivates our current work. A logical formalism is considered to be an appropriate solution to improve the flexibility and expresiveness in specifying security properties. A preliminary attempt to use logic for specifying local security properties in a constraint-based setting has been carried out [3]. Inspired by this work and the successful NPATRL [11,8], we currently explores a variant of linear temporal logic (LTL) over finite traces, -LTL, standing for pure-past security LTL [5]. In contrast to standard LTL, this logic deals only with past events in a trace. In our current work, a protocol is modelled as in previous works [9,4,3], viz. by protocol roles. A protocol role is a sequence of send and receive events, together with status events to indicate, e.g. that a protocol role has completed her protocol run. A scenario is then used to deal with the number of sessions and protocol roles considered in the analysis. Integrating -LTL into our constraint solving approach presents a challenge, since we need to develop a sound and complete decision procedure against symbolic traces, instead of concrete traces. Our idea to address this problem is by concretizing symbolic traces incrementally while deciding a formula. Basically, the decision procedure consists of two steps: transform and decide. The former step transforms a -LTL formula with respect to the current trace into a so-called elementary formula that is built from constraints and equalities using logical connectives and quantifiers. The decision is then performed by the latter step through solving the constraints and checking the equalities. Although we define a decision procedure for a fragment of -LTL, this fragment is expressive enough to specify several security properties, like various notions of secrecy and authentication, and also data freshness. We provide a Prolog implementation and have analysed several security protocols. There are many directions for improvement. From the implementation point of view, the efficiency of the decision procedure can still be improved. I would also like to investigate the expressiveness of the logic for speficying other security properties. This may result in an extension of the decision procedure for a larger fragment of the logic. Another direction is to characterize the expressivity power of -LTL compared to other security requirement languages.

KW - SCS-Cybersecurity

KW - IR-54523

KW - METIS-248138

KW - EWI-8040

U2 - 10.1007/11562931

DO - 10.1007/11562931

M3 - Conference contribution

SN - 3-540-29208-X

T3 - Electronic Notes in Theoretical Computer Science

SP - 439

EP - 440

BT - Logic Programming, 21st International Conference, ICLP 2005

A2 - Gabbrielli, M.

A2 - Gupta, G.

PB - Springer

CY - Berlin

ER -

Corin RJ, Saptawijaya A, Etalle S. PS-LTL for Constraint-Based Security Protocol Analysis. In Gabbrielli M, Gupta G, editors, Logic Programming, 21st International Conference, ICLP 2005. Berlin: Springer. 2005. p. 439-440. (Electronic Notes in Theoretical Computer Science; RFC 4080). https://doi.org/10.1007/11562931, https://doi.org/10.1007/11562931_46