ISR 2008

3rd International School on Rewriting

21 – 26 July 2008, Obergurgl, Austria

Program – Track B – Security Protocols and Term Rewriting


Hubert Comon-Lundh


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: