Deciding security of protocols against off-line guessing attacks

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. Categories and Subject Descriptors: C.2.2 [Network Protocol]: Protocol Verification, D.2.4 [Software/Program Verification]: Formal Methods, F.4.2 [Grammars and Other Rewriting Systems]: Decision Problems General Terms: Security, Theory, Verification

• Type: Conference
• Year: 2005
• Where: CCS
• Authors: Mathieu Baudet
• Keywords: CCS 2005, Off-line Guessing Attacks, Rewriting Systems, Security Privacy, Subterm Rewriting System