3rd International School on Rewriting
21 – 26 July 2008, Obergurgl, Austria
Program – Track B – Security Protocols and Term Rewriting
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.