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)
e_mail: focardi@dsi.unive.it
Dipartimento di Scienze
dell'Informazione,
Università di Bologna
Mura Anteo Zamboni 7,
I - 40127 Bologna (Italy)
e_mail: {ghelli,gorrieri}@cs.unibo.it
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.