Riccardo Focardi - Anna Ghelli - Roberto Gorrieri
Dipartimento di Matematica Applicata ed Informatica,
Università Ca' Foscari di Venezia
Via Torino 155, I - 30173 Venezia Mestre (Italy)
Dipartimento di Scienze dell'Informazione,
Università di Bologna
Mura Anteo Zamboni 7, I - 40127 Bologna (Italy)
Non interference [GM82] was originally proposed as a means for analyzing the security of computer systems. In this paper we show that its theory can be profitably exploited also for the analysis of security protocols. As a simple case study, we consider the paradigmatic example of the Needham-Schroeder public-key protocol, that was already shown incorrect and fixed in [Low96]. As expected, our analysis discovers the same bug; what is really new is the methodology, based on the idea of proving the absence of information flow between the protocol partners and potential external attackers.