Deriving the Type Flaw Attacks in the Otway-Rees Protocol by Rewriting

This paper presents an approach to formalizing and verifying security protocol specifications based on rewriting techniques. A rewrite system ${\cal R\/}_{P}$ describes the steps of a protocol and the properties under consideration, and a rewrite system ${\cal R\/}_{I}$ defines an intruder's ability of decomposing and decrypting messages. The equational theory generated by ${\cal R\/} = {\cal R\/}_{P}\,{\cup}\,{\cal R\/}_{I}$ characterizes the recognizability of terms by an intruder, i.e.~how an intruder can learn (parts of) messages exchanged among principals communicating over an insecure network. Security properties, such as authentication and secrecy, can be expressed by means of intruder's recognizability, and verifying whether a term is recognized by an intruder reduces to checking whether such a term can be rewritten to a normal form in the intruder's initial knowledge. A rewriting strategy is defined that, given a term $t$ that represents a property to be proved, suitably expands and reduces $t$ using the rules in ${\cal R\/}$ to derive whether or not $t$ is recognized by an intruder. The approach is applied on the Otway-Rees symmetric-key protocol by deriving its well-known type flaw attacks.