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.

Formalizing and Analyzing the Needham-Schroeder Symmetric-Key Protocol by Rewriting

NESI, MONICA;
2005-01-01

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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11697/12663
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? ND
social impact