Non-interference proof techniques for the analysis of cryptographic protocols

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 noninterference 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 noninterference, 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.