Using Non Interference for the Analysis of Security Protocols

Riccardo Focardi$^{\dagger}$ - Anna Ghelli$^{\ddagger}$ - Roberto Gorrieri$^{\ddagger}$

$^{\dagger}$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

$^{\ddagger}$Dipartimento di Scienze dell'Informazione,
Università di Bologna
Mura Anteo Zamboni 7, I - 40127 Bologna (Italy)
e_mail: {ghelli,gorrieri}@cs.unibo.it

Abstract:

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.