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 ${\cal R\/}$ describes the steps of the protocol and an intruder's ability of decomposing and decrypting messages, and a tree automaton ${\cal 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 ${\cal R\/}$ and the transitions in ${\cal 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.
Titolo: | Formalizing and Analyzing the Needham-Schroeder Symmetric-Key Protocol by Rewriting |
Autori: | |
Data di pubblicazione: | 2005 |
Rivista: | |
Abstract: | 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 ${\cal R\/}$ describes the steps of the protocol and an intruder's ability of decomposing and decrypting messages, and a tree automaton ${\cal 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 ${\cal R\/}$ and the transitions in ${\cal 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. |
Handle: | http://hdl.handle.net/11697/12663 |
Appare nelle tipologie: | 1.1 Articolo in rivista |