Hubert Comon-Lundh, Stéphanie Delaune, and Jonathan K. Millen. Constraint solving techniques and enriching the model with equational theories. In Véronique Cortier and Steve Kremer, editors, * Formal Models and Techniques for Analyzing Security Protocols*, Cryptology and Information Security Series, pp. 35–61, IOS Press, 2011.

Derivability constraints represent in a symbolic way the infinite set of possible executions of a finite protocol, in presence of an arbitrary active attacker. Solving a derivability constraint consists in computing a simplified representation of such executions, which is amenable to the verification of any (trace) security property. Our goal is to explain this method on a non-trivial combination of primitives.

In this chapter we explain how to model the protocol executions using derivability constraints, and how such constraints are interpreted, depending on the cryptographic primitives and the assumed attacker capabilities. Such capabilities are represented as a deduction system that has some specific properties. We choose as an example the combination of exclusive-or, symmetric encryption\slashdecryption and pairing\slashunpairing. We explain the properties of the deduction system in this case and give a complete and terminating set of rules that solves derivability constraints. A similar set of rules has been already published for the classical Dolev-Yao attacker, but it is a new result for the combination of primitives that we consider. This allows to decide trace security properties for this combination of primitives and arbitrary finite protocols.

@incollection{CDM-fmtasp11, abstract = {Derivability constraints represent in a symbolic way the infinite set of possible executions of a finite protocol, in presence of an arbitrary active attacker. Solving a derivability constraint consists in computing a simplified representation of such executions, which is amenable to the verification of any (trace) security property. Our goal is to explain this method on a non-trivial combination of primitives.\par In this chapter we explain how to model the protocol executions using derivability constraints, and how such constraints are interpreted, depending on the cryptographic primitives and the assumed attacker capabilities. Such capabilities are represented as a deduction system that has some specific properties. We choose as an example the combination of exclusive-or, symmetric encryption{\slash}decryption and pairing{\slash}unpairing. We explain the properties of the deduction system in this case and give a complete and terminating set of rules that solves derivability constraints. A similar set of rules has been already published for the classical Dolev-Yao attacker, but it is a new result for the combination of primitives that we consider. This allows to decide trace security properties for this combination of primitives and arbitrary finite protocols.}, author = {Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie and Millen, Jonathan K.}, booktitle = {Formal Models and Techniques for Analyzing Security Protocols}, editor = {Cortier, V{\'e}ronique and Kremer, Steve}, pages = {35-61}, publisher = {{IOS} Press}, series = {Cryptology and Information Security Series}, title = {Constraint solving techniques and enriching the model with equational theories}, volume = {5}, year = {2011}, lsv-category = {chap}, wwwpublic = {public and ccsb}, }