CINECA IRIS Institutional Research Information System
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishThis 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 |
File in questo prodotto:
Copyright © 2021