Using Formal Methods for Analyzing Security

Edmund Clarke          Will Marrero Department of Computer Science Carnegie Mellon University Pittsburgh, PA 15213-3891 {emc, marrero}@cs.cmu.edu     Whether it be finite-state machines, Markov models, timed-automata, or some other formalism, formal methods have proven to be useful in analyzing and debugging complex systems. Formal methods have been used (and continue to be used) to analyze systems as diverse as automobile control systems, aviation control systems, chemical processes, communication protocols, railway signalling systems, and computer hardware. One formal method in particular, model checking, has enjoyed great success in the field of electronic circuit verification. This technique involves modelling a circuit as a finite state machine and examining all possible execution traces of the machine to determine if there are any undesirable traces. Model checking has found a number of errors in real world designs. It has been so useful in large part because of the complexity of the hardware designs analyzed. In general, formal methods can make a significant contribution to the analysis of complex systems that are difficult to reason about otherwise, and which may contain subtle errors. It is our belief that computer security and information survivability are such areas. A number of researchers have already begun to investigate the possibility of using formal methods for analyzing authentication protocols. Steps have also been taken towards trying to verify electronic commerce protocols. We believe that model checking, as well as formal methods in general, will prove useful in trying to analyze and debug systems which try to assure security and information survivability.
    One of the earliest successful attempts at formally reasoning about security protocols involved developing a new logic in which one could express and deduce security properties. The earliest such logic is commonly referred to as the BAN logic and is due to Burrows, Abadi, and Needham. Their syntax provided constructs for expressing intuitive properties like "A said X," "A believes X," "K is a good key," and "S is an authority on X." They also provide a set of proof rules which can then be used to try to deduce security properties like ``A and B believe K is a good key'' from a list of explicit assumptions made about the protocol. This formalism was successful in uncovering implicit assumptions and some weaknesses in a number of protocols. However, this logic has been criticized for the "protocol idealization" step required when using this formalism. Protocols in the literature are typically given as a sequence of messages. Use of the BAN logic requires that the user transform each message in the protocol into formulas about that message, so that the inferences can be made within the logic. For example, if the server sends a message containing the key Kab, then that step might need to be converted into a step where the server sends a message that explicitly states that the key Kab is a good key for communication between A and B. There have been attempts to improve and expand this logic as well as attempts to give this logic a rigorous semantics . The BAN logic remains popular because of its simplicity and high level of abstraction.
    Recent work in the use of modal logics for verifying security protocols includes the development of a logic that can express accountability. Kailar convincingly argues that in applications such as electronic commerce, it is accountability and not belief that is important. Like their counterparts in the paper world, one would like people to be held accountable for their electronic transactions. This means that it is not enough for the individual participants to believe that a transaction is taking place. They must be able to prove to a third party that a transaction is taking place. Kailar provides a syntax which allows such properties to be expressed and a set of proof rules for verifying them. Similar to the BAN logic, Kailar's accountability logic is at a very high level of abstraction. Still, Kailar is able to use it to analyze four protocols and to find a lack of accountability in a variant of one of CMU's Internet Billing Server Protocols.
    An orthogonal line of research involves trying to automate the process of verification when using these logics. Craigen and Saaltink attempt this by embedding the BAN logic in EVES. By building a forward-chaining mechanism and changing some of the rules, they were able to build a system that would try to develop the entire theory of a set of axioms (find the closure of a set of formulas under the derivation rules). Kindred and Wing went further by proposing a theory-checker generator. They provide a formal and well defined framework with assurances about correctness and termination. In addition, their system generates theory checkers for a variety of logics including BAN, AUTLOG, and Kailar's accountability logic. In more recent work they have also tried formalizing the "idealization" step required when using these logics.
    The other research in this area has a more operational emphasis. These techniques involve formalizing the execution of a protocol into a set of traces allowed by the protocol. Typically, they also allow for interference by a malicious adversary with certain well defined capabilities which typically include concatenating messages together and breaking a concatenated message apart into its components, as well as encrypting and decrypting with known keys. The first attempt at such a formalism is due to Dolev and Yao. In their system, one formalizes the operations available to the adversary, both the inherent ones and the "derived" operations that result from using the honest particpants as oracles. Their system then searches for a sequence of operations in this algebra that would allow the adversary to gain knowledge of information that is supposed to be protected.
    Meadows used an extension of the Dolev-Yao model in her PROLOG based model checker, the NRL Protocol Analyzer. In her system, the user models a protocol as a set of rules that describe how an intruder generates knowledge. These rules model both how the intruder can generate knowledge on its own by applying encryption and decryption, and how the intruder can generate new knowledge by receiving responses to messages it sends to the honest principals participating in the protocol. To perform the verification, the user also supplies a description of an insecure state. The model checker then searches backwards in an attempt to find an initial state. This is accomplished naturally in PROLOG by attempting to unify the current state against the right hand side of a rule and thus deducing from the left hand side what the state description for the previous state must be. If the initial state is found, then the system is insecure, otherwise an attempt is made to prove that the insecure state is unreachable by showing that any state that leads to this particular state is also unreachable. The advantage of this backwards search is that the user need not specify a specific number of protocol sessions or runs ahead of time. On the other hand, this method is not guaranteed to terminate.
    In a related approach, Bella and Paulson have developed an inductive proof method based on the same Dolev-Yao model. They provide a set of rules that inductively define the set of valid traces for a protocol. Each rule has the form, if tr is a valid trace and if tr satisfies some conditions C, then tr^X is also a valid trace where X is some specific action taken by one of the principals, including possibly the adversary. The structure of X usually also depends on tr itself. They also provide a description of an insecure trace and then use Isabelle to prove that there is no valid trace (allowed by the protocol) that is also an insecure trace (contains an attack). By using this method they were able to prove the correctness of their models without bounding the number of sessions or runs. The drawback to this method is that it is not clear what kind of feedback the user can get if Isabelle fails to find a proof.
    Other recent work in this area has involved trying to use generic model checking tools to verify security protocols. Lowe uses the FDR model checker for CSP to analyze the Needham-Schroeder Public-Key Authentication Protocol. Lowe succeeded in finding a previously unpublished error in the protocol. Since this initial work, Lowe has implemented CASPER, a front end to FDR which allows the user to describe a protocol is an easier modelling language. Mitchell and others have linvestigated the use of Murphi, a state space exploration tool, to verify security protocols. They have analyzed a number of authentication protocols as well as the Secure Socket Layer protocol. The fact that these researchers have been able to use already existing generic model checkers is promising, although we believe that more can be done with a special purpose tool.
    We also have investigated how to use model checking to analyze security protocols. We have developed a special purpose model checker for this problem domain. In our system, each honest participant in a protocol is modelled as a process consisting of a sequence of actions that defines that participant's role in the protocol, and a set of variable bindings that are created when a participant receives a message. The adversary then intercepts all messages and can generate new messages using the capabilities in the Dolev-Yao model. These capabilities are modelled using a message derivation engine which tries to create messages that honest participants are willing to receive. This message derivation engine allows us to check what the adversary (or any participant for that matter) knows at any time. Finally, we allow user defined internal actions which can be used to mark important points in the protocol, for example, when the bank debits an account or when a customer commits to a transaction.
    Unlike the other model checking systems described above, we also provide a logic as a specification language. This logic can be used to express relationships between events and between the variable bindings belonging to the different agents. In addition, however, we can also express properties involving knowledge. Because the manipulation of knowledge (messages) is built into our tool, this kind of checking is straightforward. As we shall see, this logic is expressive enough to cover a wide variety of properties including authentication, secrecy, anonymity, and correspondence.
    A simplified electronic commerce protocal example loosely based on the iKP will help to illustrate our ideas. In the example below, the fields have the following meaning.

DESC - the description of the goods desired by the customer
PRICE - the price the merchant is charging for those goods
K - a key newly generated by the customer
M - the merchants ID
TID - a locally unique transaction ID generated by the merchant
CC# - the customer's credit card number
{X}_public(Y) - X encrypted with Y's public key
{X}_sig(Y) - X signed with Y's private key

The protocol proceeds as follows where C is the customer, M is the merchant, and A is the credit card authority:

1. Cutomer asks for price and provides session key
C -> M : {DESC, K}_public(M)
2. Merchant replies with price and transaction ID
M -> C : {PRICE, TID}_K
3. Customer sends payment information (Cusotmer commit point)
C -> M : {{CC#, PRICE, M, TID}_public(A), TID}_K
4. Merchant requests payment authorization (Merchant commit point)
M -> A : {{CC#, PRICE, M, TID}_public(A), PRICE, M, TID}_public(A)
5. Authority authorizes payment (Authority commit point)
A -> M : {PRICE, M, TID}_sig(A)
6. Merchant supplies receipt
M -> C : {PRICE, M, TID}_sig(A)

The description of the customer would be as follows, where constants are given in uppercase and variables are given in lowercase followed by their type.

send:         {DESC, K}_public(M)
receive:    {price:data, tid:data}_K
authorize: (price:data)
send:         {{CC#, price:data, M, tid:data}_public(A), tid:data}_K
receive:    {price:data, M, tid:data}_sig(A)

The lowercase variables are bound during the execution of the protocol when the customer receives a message of the correct type. For example, in step 2, the customer is willing to receive any message consisting of two data items encrypted with the key K. These items are then bound to the respective variables and used throughout the rest of the protocol. The authorize action in step 3 is an internal action used to mark the customer's commit point in the protocol so that the specification can refer to it. The description of the customer and credit card authority are given in a similar fashion.
Due to space limitations we will not give the syntax and semantics of the specification logic here, but we will give examples of the kinds of properties that can be checked.

Authorization of transaction by customer: If the credit card authority debits the account CC# by the amount PRICE, then sometime in the past, the customer with account CC# has performed an authorize action of the form authorize (PRICE).
Authorization of transaction by merchant: If the credit card authority credits the merchant by the amount PRICE, then sometime in the past the merchant must have requested this payment.
The customer's credit card number is not revealed: If some principal P knows the credit card number CC#, then P must be either the customer C or the credit card authority A.
Privacy/Anonymity of the customer: If some principal P knows the identity of the customer C, then P must be either the customer or the credit card authority. If some principal P knows the description of the goods DESC, then P must be the customer or the merchant. (Therefore the only one that knows both the customer's identity and the description of the goods is the customer).

This is a simple example of how model checking can be useful in the analysis of protocols. These kinds of formal methods have already uncovered errors and weaknesses in previously published security protocols. It is our belief that these kinds of techniques can be applied to more complex systems and in particular to analyze information survivability issues. To our knowledge, this has yet to attempted. The size of the systems to be verified will pose a challenge. These security protocols already generate a very large state space. State space reduction techniques will most likely be necessary when analyzing information survivability. It also remains to be seen what extensions may be necessary to these tools in order to handle the kinds of problems encountered in information survivability.