Constraint solving techniques and enriching the model with equational theories
Comon-Lundh Hubert, Delaune St eacute phanie, Millen Jonathan K. · IOS Press eBooks · 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.