Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions

Abstract. We consider the problem of deciding the security of cryptographic protocols for a bounded number of sessions, taking into account some algebraic properties of the security primitives, for instance Abelian group properties. We propose a general method for deriving decision algorithms, splitting the task into 4 properties of the rewriting system describing the intruder capabilities: locality, conservativity, finite variant property and decidability of one-step deducibility constraints. We illustrate this method on a non trivial example, combining several Abelian Group properties, exponentiation and a homomorphism, showing a decidability result for this combination.

• Type: Conference
• Year: 2009
• Where: RTA
• Authors: Sergiu Bursuc, Hubert Comon-Lundh
• Keywords: Abelian Group Properties, Instance Abelian Group, One-step Deducibility Constraints, RTA 2009, Theoretical Computer Science