Analysis of Cryptographic Protocols with a
Concatenation of Techniques
Masters Thesis Prospectus
As the frequency and importance of network transactions grows, so does the need for security. This security can be provided by cryptography and protocols designed to guarantee secure interaction. However, these protocols have the potential to contain flaws that might endanger the security of the transactions they are supposed to guarantee. Many methods of verification have been proposed to raise the level of confidence in these protocols. In this work, we will use a tool that combines two of these methods to analyze a set of cryptographic protocols. Through this process we hope to learn more about the characteristics of these protocols and the tool, discover ways to extend the abilities of our technique, and use the aggregate results to make generalizations about cryptographic protocols and the tool used to analyze them.
Cryptography provides many of the tools necessary to ensure security in networks. In addition to the secrecy provided by encryption, cryptographic protocols provide authentication, integrity, and non-repudiation [SCH96]. Without these tools, messages can not be delivered or received from specific individuals, be made tamper proof, or be attributed to an individual. These facilities allow a wide range of transactions to be undertaken on a network with comparative safety.
Although cryptographic protocols can enable secure interaction over a network, there is a difficulty. A protocol is just series of actions between two principals, similar to an algorithm or a program. Therefore, cryptographic protocols are subject to the flaws that all programs and algorithms may contain. Although there is no algorithm to determine the security of all protocols, much effort has been expended in the search for techniques that could aid in the discovery of flaws in cryptographic protocols as in [BAN90], [MED96], & [SVO94]. These techniques can be grouped into these four categories, expert systems, algebraic term rewriting, program verification methods, and logical analysis [MED92]. The first three techniques evaluate the data and actions of the principals to be evaluated, while the last technique, logical analysis, allows the beliefs of the principals to be examined. The combination of a technique from program verification called Weakest Precondition reasoning [DIJK76] with BAN logic [BAN90] has been proposed to create one tool that can examine the data, actions, and beliefs of a protocol more completely and efficiently than the techniques could do by themselves [YW99].
We propose to carry out this combination of techniques and use it to evaluate a set of published protocols. Here is a simple explanation of the process used to analyze each protocol. The data and actions will be translated into the formal language of the tool. Then the tool can evaluate this language to produce a formal definition. The tool facilitates the use of the PVS Proof Checker [ORS92] with axioms provided by the logic to prove and simplify the definition produced by the tool. This process and its result provide insight into the characteristics of the analyzed protocol.
We propose to survey a wide range of protocols such as IKE, SET, SSH, SHTML, X.509, Needham-Schroeder, Denning-Sacco, Kerberos and others. This will allow us to gather new information about individual protocols, gain experience and knowledge about the use of the tool as each protocol is analyzed, and provide results which can be analyzed for general patterns in cryptographic protocols and the tool’s output. As it is implemented with a range of protocols we will extend the tool’s capabilities to handle new operations. We hope our use of the tool will elicit previously unrecognized flaws in the protocols. Some of the information gathered may help us to streamline protocols by pointing out useless or redundant actions. Other protocol actions may provide more security than is necessary according to the protocol’s definition. We expect to gather two types of information from this process. These are new flaws or information, or previously discovered flaws or protocol characteristics. Both types of information allow us to evaluate the effectiveness of the tool. The soundness of the technique can be gauged by its ability to find already known flaws, weaknesses, and characteristics of previously analyzed protocols. Discovery of new information will demonstrate the tool’s ability to find unknown characteristics of protocols. The process of evaluating the protocols will also serve as a means to determine the effectiveness of the tool and reveal whether the tool is easy to use, and extend.
When the analysis of the protocols is complete, we will have a body of information that can be analyzed. If patterns in this data can be discerned, we can also make useful generalizations about the flaws that the protocols are prone to exhibit. This should also help us understand the type and quality of information the tool can provide. Guidelines for the proper design of correct and secure cryptographic protocols could be generated to avoid any typical flaws or inefficiencies found in the protocols.
Cryptographic protocols demand a high level of assurance as to their correct and secure operation. In an effort to verify these protocols, many techniques have been developed to analyze cryptographic protocols. We propose to use a tool that combines two of these techniques so that the data, actions and beliefs of the principals can be examined. A survey of protocols with this tool will provide useful information about cryptographic protocols, necessary extensions to the tool, and the effectiveness of technique we propose.
[BAN90] - Burrows, M. Abadi, M., and Needham, R. M. "A logic of Authentication", ACM Transactions on Computer Systems Review, vol 8, no. 1, Feb 1990, pp 18-36
[DIJK76] - Dijkstra, E. W. "A Discipline of Programming", Prentice Hall Series in Automatic Computation, Prentice-Hall Inc. Englewood Cliffs, NJ, 1976
[MED92] – Meadows, C. "Applying Formal Methods to the Analysis of a Key Management Protocol" Journal of Computer Security Foundations Workship VII, IEEE Computer Society Press, 1994, pp. 84-89
[MED96] - Meadows, C. The NRL Protocol Analyzer: An Overview. Journal of Logic Programming, 26(2): pp 113-131, 1996.
[NS78] - Needham, R. M. & Schroeder, M. D. "Using Encryption for Authentication in Large Networks of Computers" Communications of the ACM, vol 21, no. 12, Dec 1978, pp 993-999
[ORS92] - Owre, S. Rushby, J. M. Shankar, N. "PVS - A Prototype Verification System" Lecture Notes in Artificial Intelligence" no. 607, pp 748-752, 1992
[SCH96] - Schneier, B. "Applied Cryptography: Protocols, Algorithms, and Source Code in C", John Wiley & Sons Inc. New York, NY, 1996
[SVO94] - Syverson, P. F. van Oorschot, P. C. "On Unifying Some Cryptographic Protocol Logics" IEEE Symposium on Security and Privacy 1994
[YW99] - Yasinsac, A & Wulf, W. A. "Framework for a Cryptographic Protocol Evaluation Workbench" , to appear in the Proceedings of the Fourth IEEE Symposium on High Assurance Systems Engineering (HASE) '99, Nov 17-19, 99, Washington, D.C.