Application of Dependency Graphs to Security Protocol Analysis
We present a computationally sound technique of static analysis for confidentiality in cryptographic protocols. The technique is a combination of the dependency flow graphs presented by Beck and Pingali and our earlier works – we start with the protocol r
- PDF / 274,276 Bytes
- 18 Pages / 430 x 660 pts Page_size
- 79 Downloads / 173 Views
Tallinn University of Technology 2 Tartu University 3 Cybernetica AS
Abstract. We present a computationally sound technique of static analysis for confidentiality in cryptographic protocols. The technique is a combination of the dependency flow graphs presented by Beck and Pingali and our earlier works – we start with the protocol representation as a dependency graph indicating possible flows of data in all possible runs of the protocol and replace the cryptographic operations with constructions which are “obviously secure”. Transformations are made in such a way that the semantics of the resulting graph remains computationally indistinguishable from the semantics of the original graph. The transformed graphs are analysed again; the transformations are applied until no more transformations are possible. A protocol is deemed secure if its transformed version is secure; the transformed versions are amenable to a very simple security analysis. The framework is well-suited for producing fully automated (with zero user input) proofs for protocol security.
1
Introduction
A protocol is a convention that enables the connection, communication, and data exchange between several computing entities. A cryptographic protocol is a protocol, which performs some security-related function and applies cryptographic methods. Naturally, the cryptographic protocol is expected to satisfy certain security properties. Examples of those properties could be confidentiality, integrity, and so on. Therefore there is a need for methods for indicating whether the given protocol satisfies the given security property or not. The latter is simpler than the first – having an example of successful attack breaching the property of interest is sufficient to show that the protocol does not satisfy it. Showing that the protocol is secure with respect to certain properties is essentially convincing that no attack (known or unknown) breaching these properties exist. In this paper we propose a framework for examining the protocol security properties based on the notion of computational indistinguishability, assuming certain properties of cryptographic operations. Currently the framework is used for checking the preservation of confidentiality and integrity properties in protocols. In principle, the framework should be suitable for verifying all properties whose fulfilment can be observed by the protocol participants and/or the adversary — the transformation process does not change the observable properties of protocols. G. Barthe and C. Fournet (Eds.): TGC 2007, LNCS 4912, pp. 294–311, 2008. c Springer-Verlag Berlin Heidelberg 2008
Application of Dependency Graphs to Security Protocol Analysis
295
The basis of the analysis – protocol semantics and the set of assumptions on the cryptographic operations we used – is similar to [18,27], while the protocol language is much more powerful, and the analysis methodology is significantly different. Our contribution is the introduction of the support for the replication to the analysed protocols, and using the approach
Data Loading...
