Non-interference proof techniques for the analysis of cryptographic protocols

Issue title: WITS'03

Guest editors: Roberto Gorrieri

Article type: Research Article

Authors: Bugliesi, Michele | Rossi, Sabina

Affiliations: Dipartimento di Informatica, Università Ca' Foscari di Venezia, via Torino 155, 30172 Venezia, Italy. E-mail: [email protected], [email protected]

Abstract: Non-interference has been advocated by various authors as a uniform framework for the formal specification of security properties in cryptographic protocols. Unfortunately, specifications based on non-interference are often non-effective, as they require protocol analyses in the presence of all possible intruders. This paper develops new characterizations of non-interference that rely on a finitary representation of intruders. These characterizations draw on equivalence relations built on top of labelled transition systems in which the presence of intruders is accounted for, indirectly, in terms of their (the intruders') knowledge of the protocols' initial data. The new characterizations apply uniformly to trace and bisimulation non-interference, yielding proof techniques for the analysis of various security properties. We demonstrate the effectiveness of such techniques in the analysis of different properties of a fair exchange protocol.

Keywords: Process calculi, concurrency, behavioral equivalences, security

DOI: 10.3233/JCS-2005-13104

Journal: Journal of Computer Security, vol. 13, no. 1, pp. 87-113, 2005