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(1) (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(1) (1994/1995) 5–33; IEEE Trans. Software Eng. 23(9) (199) 550–571). This allows for the comparison between such aproperty and the one based on CSP, which was already recast under the general scheme of Focardi and Martinelli (1999).