Introduction

One area of major successes for formal methods has been the verification of security protocols. A number of specialized tools have been developed in the last decade that have exposed subtle flaws in existing protocols (see, e.g. [6, 7]). For the most part, however, these tools have been used by the researchers that developed them, and less attention has been paid to usability issues.

We have developed a new approach to formulating and checking cryptographic protocols. It does not enable any new form of analysis. Instead, it makes verification more accessible to the designers of protocols. Its key contribution is a new characterization of these protocols that is both closer to how designers conceive them, and amenable to a direct encoding in standard first-order logic. This more direct encoding allows existing tools to be applied as black boxes without modification; it requires no tweaking of parameters or issuing of special directives by the user. Moreover, because the semantic gap between informal descriptions of protocols and their formalization is smaller, there are fewer opportunities for errors to creep in.

Approach

Our approach, which we call knowledge flow analysis, gives a uniform framework for expressing the actions of principals, assumptions on intruders, and properties of cryptographic primitives. The dynamic behavior of the protocol is described by an initial state of knowledge, and a collection of rules that dictate how knowledge may flow amongst principals. A state is given by a relation mapping principals to the values they know; the allowable knowledge flows can thus be succinctly described as a standard transition relation on knowledge states, written as a constraint.

The Alloy modeling language [5] is used to record the details of the protocol and its security goals, and the Alloy Analyzer [4] is used to find flaws. We have implemented a generic Alloy framework with a library of primitives that can be easily instantiated for a variety of protocols. The approach, however, requires no special features of Alloy or its analysis, and could be applied in the context of any formal method based on first-order logic.

Results

The knowledge flow approach allows us to model a range of intruder capabilities and to detect replay, parallel session, type flaw, and binding attacks. We have applied it to both symmetric and public-key cryptography under the Dolev-Yao [2] model and obtained the following results:

• a reproduction of the parallel session attack [6] on the Needham-Schroeder [8] protocol;
• a reproduction of the type flaw attack [1] on the Otway-Rees [9] protocol;
• a proof that the modified Needham-Schroeder [6] protocol is secure against all attacks that use at most two parallel sessions; and
• a proof that the CPUF Renewal and Bootstrapping [3] protocols are secure for an unbounded number of parallel sessesions.

This approach grew out of an effort to check the CPUF-based key management protocols. It is the final result of a series of incremental attempts at formalizing and checking the protocols using the Alloy language and tool. This process helped crystallize our intuitions, and drew out a number of important assumptions. For example, we found that we must assume that communication rules do not involve values that are fixed points of cryptographic functions such as hashing, encryption, etc.

Research Support

This work is supported in part by grant 0086154 (Design Conformant Software) from the ITR program of the National Science Foundation.

References

[1] M. Burrows, M. Abadi, and R. Needham. A logic of authentication. ACM Trans. Comput. Syst., 8(1), pp. 18--36, 1990.

[2] D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2), pp. 198--208, 1983.

[3] B. L. P. Gassend. Physical random functions. Master's thesis, MIT, 2003.

[4] D. Jackson. Automating first-order relational logic. In Proc. ACM SIGSOFT Conf. Foundations of Software Engineering / European Software Engineering Conference (FSE/ESEC '00), 2000.

[5] D. Jackson. Alloy: a lightweight object modelling notation. ACM TOSEM, 11(2), pp. 256--290, 2002.

[6] G. Lowe. Casper: A compiler for the analysis of security protocols. In Proceedings of the 1997 IEEE Computer Society Symposium on Research in Security and Privacy, pp. 18--30, 1997.

[7] J. Mitchell, M. Mitchell, and U. Stern. Automated analysis of cryptographic protocols using muro. In Proceedings of the 1997 IEEE Symposium on Research in Security and Privacy, pp. 141-153, 1997.

[8] R. Needham and M. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12), pp. 993--999, 1978.

[9] D. Otway and O. Rees. Efficient and timely mutual authentication. Operating Systems Review, pp. 8--10, January 1987.