This paper reports on work in progress on using rewriting techniques for the specification and the verification of communication protocols. As in Genet and Klay's approach to formalizing protocols, a rewrite system R describes the steps of the protocol and an intruder's ability of decomposing and decrypting messages, and a tree automaton A encodes the initial set of communication requests and an intruder's initial knowledge. In a previous work we have defined a rewriting strategy that, given a term t that represents a property of the protocol to be proved, suitably expands and reduces t using the rules in R and the transitions in A to derive whether or not t is recognized by an intruder. In this paper we present a formalization of the Needham-Schroeder symmetric-key protocol and use the rewriting strategy for deriving two well-known authentication attacks. © 2005 Elsevier B.V. All rights reserved.
Nesi, M., & Rucci, G. (2005). Formalizing and analyzing the Needham-Schroeder symmetric-key protocol by rewriting. In Electronic Notes in Theoretical Computer Science (Vol. 135, pp. 95–114). Elsevier. https://doi.org/10.1016/j.entcs.2005.06.002