A comparison of three authentication properties

Authentication is a slippery security property that has been formally defined only recently; among the recent definitions, two rather interesting ones have been proposed for the spi-calculus by (Abadi and Gordon (in: Proc. CONCUR'97, Lecture Notes in Computer Science, Vol. 1243, Springer, Berlin, 1997, pp. 59-73; Inform. and Comput. 148(l) (1999) 1-70) and for CSP by Lowe (in: Proc. 10th Computer Security Foundation Workshop, IEEE Press, 1997, pp. 31-43). On the other hand, in a recent paper (in: Proc. World Congr. on Formal Methods (FM'99), Lecture Notes in Computer Science, Vol. 1708, Springer, Berlin, 1999, pp. 794-813), we have proved that many existing security properties can be seen uniformly as specific instances of a general scheme based on the idea of non-interference. The purpose of this paper is to show that, under reasonable assumptions, spi-authentication can be recast in this general framework as well, by showing that it is equivalent to the non-interference property called NDC of Focardi and Gorrieri (J. Comput. Security 3(l) (1994/1995) 5-33; IEEE Trans. Software Eng. 23(9) (199) 550-571). This allows for the comparison between such a property and the one based on CSP, which was already recast under the general scheme of Focardi and Martinelli (1999). (C) 2002 Elsevier Science B.V. All rights reserved.