The article discusses the issues of modeling and the analysis of executions, which is a substantial part of modern communication protocols - authentication protocols, which are generally referred to herein as security protocols. The article presents a way of security protocols executions analysis with the use of probabilistic automata, without well known and widely used perfect cryptography assumption (we assume allowing the possibility of breaking a key with a specified probability). This type of analysis leads to interesting observations about the operation of the protocol and its weaknesses.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.