A logic of authentication Export

@article{citeulike:4959676, abstract = {Questions of belief are essential in analyzing protocols for the authentication of principals in distributed computing systems. In this paper we motivate, set out, and exemplify a logic specifically designed for this analysis; we show how various protocols differ subtly with respect to the required initial assumptions of the participants and their final beliefs. Our formalism has enabled us to isolate and express these differences with a precision that was not previously possible. It has drawn attention to features of protocols of which we and their authors were previously unaware, and allowed us to suggest improvements to the protocols. The reasoning about some protocols has been mechanically verified. This paper starts with an informal account of the problem, goes on to explain the formalism to be used, and gives examples of its application to protocols from the literature, both with shared-key cryptography and with public-key cryptography. Some of the examples are chosen because of their practical importance, while others serve to illustrate subtle points of the logic and to explain how we use it. We discuss extensions of the logic motivated by actual practice---for example, in order to account for the use of hash functions in signatures. The final sections contain a formal semantics of the logic and some conclusions. SRC Research Report 39 was originally published on February 28, 1989, and revised on February 22, 1990. This is the main body of the revised version. An appendix to the revised version is available separately. c flDigital Equipment Corporation 1989, 1990 This work may not be copied or reproduced in whole or in part for any commercial}, author = {Burrows, Michael and Abadi, Martin and Needham, Roger}, citeulike-article-id = {4959676}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.6628}, journal = {ACM Transactions on Computer Systems}, keywords = {authentication, logic, security}, pages = {18--36}, posted-at = {2009-06-25 19:17:15}, priority = {2}, title = {A logic of authentication}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.6628}, volume = {8}, year = {1990} }

TY - JOUR ID - citeulike:4959676 L3 - citeulike-article-id:4959676 N2 - Questions of belief are essential in analyzing protocols for the authentication of principals in distributed computing systems. In this paper we motivate, set out, and exemplify a logic specifically designed for this analysis; we show how various protocols differ subtly with respect to the required initial assumptions of the participants and their final beliefs. Our formalism has enabled us to isolate and express these differences with a precision that was not previously possible. It has drawn attention to features of protocols of which we and their authors were previously unaware, and allowed us to suggest improvements to the protocols. The reasoning about some protocols has been mechanically verified. This paper starts with an informal account of the problem, goes on to explain the formalism to be used, and gives examples of its application to protocols from the literature, both with shared-key cryptography and with public-key cryptography. Some of the examples are chosen because of their practical importance, while others serve to illustrate subtle points of the logic and to explain how we use it. We discuss extensions of the logic motivated by actual practice---for example, in order to account for the use of hash functions in signatures. The final sections contain a formal semantics of the logic and some conclusions. SRC Research Report 39 was originally published on February 28, 1989, and revised on February 22, 1990. This is the main body of the revised version. An appendix to the revised version is available separately. c flDigital Equipment Corporation 1989, 1990 This work may not be copied or reproduced in whole or in part for any commercial JF - ACM Transactions on Computer Systems EP - 36 TI - A logic of authentication VL - 8 SP - 18 KW - authentication KW - logic KW - security AU - Burrows, Michael AU - Abadi, Martin AU - Needham, Roger PY - 1990/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.6628 ER -