Deciding security of protocols against off-line guessing attacks
Mathieu Baudet · 2005
We provide an effective procedure for deciding the existence of off-line guessing attacks on security protocols, for a bounded number of sessions.The procedure consists of a constraint solving algorithm for determining satisfiability and equivalence of a class of second-order E-unification problems, where the equational theory E is presented by a convergent subterm rewriting system.To the best of our knowledge, this is the first decidability result to use the generic definition of off-line guessing attacks due to Corin et al. based on static equivalence in the applied pi calculus.