The Completeness Theorem for a Logic of Authentication

• Autorzy: Kurkowski, M.
• Języki publikacji: EN

Abstrakty

EN

In a distributed computational system, security depends heavily on the use of secure protocols such as authentication protocols. In the past few years, a lot of attention has been paid to the use of special logics to analyze cryptographic authentication protocols. Burrows, Abadi, Needham and others have proposed a few logics for the analysis of these protocols (called BAN-Iogics). These are specialized versions of modal logics of belief, with special constructs for expressing some of the central concepts used in authentication processes. These logics have revealed many subtleties and serious flaws in published and widely applied protocols. Unfortunately, they have also created some confusions, for example they are not complete. In the present paper we introduce a new logic of authentication, which is a modification of the BAN logic. It provides a convenient formal language for specifying and reasoning about cryptographic protocols requirements. We also provide an axiomatic inference system, a model of computation and semantics. We present some important properties of our logic, first of all the Completeness Theorem.

Słowa kluczowe

PL

protokoły uwierzytelniania; rozproszony system; logika uwierzytelniania

EN

authentication protocols; distributed system; authentication logic

• Czasopismo: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
• Rocznik: 2000/2001
• Tom: Vol. 8
• Strony: 37--44
• Opis fizyczny: Bibliogr. 7 poz.

Twórcy

autor

Kurkowski, M.

• Institute of Mathematics and Computer Science Pedagogical University of Częstochowa,

Bibliografia

• [1] [NS78] Needham R., Schroeder M., Using encryption for authentication in large networks of computers, Communications of the ACM, 21(12), (1978) pp. 993-999.
• [2] [BAN89] Burrows M., Abadi M. and Needham R. A logic of authentication. Research Report 39, Digital Systems Research Center, February 1989.
• [3] [GNY90] Gong L., Needham R., Yahalom R., Reasoning about belief in cryptographic protocols, In Proceedings of the 1990 IEEE Symposium on Security and Privacy, (1990) pp. 234-248, IEEE Computer Society Press.
• [4] [AT91] Abadi M. and Tuttle M. A semantics for a logic of authentication. In Proceedings of the tenth ACM Symposium on Principies of Distributed Computing, pp. 201 - 216, ACM Press, August 1991.
• [5] [S91] Syverson P., The use of logic in the analysis of cryptographic protocols, In Proceedings of the 1991 IEEE Computer Security Symposium on Security and Privacy, (1991) pp. 156-170, IEEE Computer Society Press.
• [6] [SM93] Syverson P., Meadows C., A logical language for specifying cryptographic protocol requirements, In Proceedings of the 1993 IEEE Computer Security Symposium on Security and Privacy, (1993) pp. 165- 177, IEEE Computer Society Press.
• [7] [Sv094] Syverson P., van Oorschot P.C., On unifying some cryptographic protocol logics, In Proceedings of the 1994 IEEE Computer Security Foundations Workshop VII, (1994) pp. 14-29, IEEE Computer Society Press.