3rd International School on Rewriting

21 – 26 July 2008, Obergurgl, Austria

Program – Track B – Security Protocols and Term Rewriting

Lecturer

Hubert Comon-Lundh

Introduction

Automated security proofs is an area in which it is hard to avoid using term rewriting systems. There are two reasons: first algebraic properties of cryptographic primitives are defined by an equational theory. Also, it is easier to define the intruder deduction problem as, given s and t, find a context C such that C[s] rewrites to t. This yields new interesting problems in term rewriting, which have been studied during the past decade.

A tentative summary of the lecture:

• examples of security protocols and attacks,
• formal definitions of attacks: term rewriting and equational theories come into the picture,
• examples of relevant equational theories,
• the passive attacker case: locality theorems, general decidability and complexity results (depending on the properties of the term rewriting system),
• the active attacker case: small attacks theorems,
• other security properties: deciding static equivalence.

Material

• slides