Cryptographically Faithful Proofs of Security Protocols

Status

This project started in February 2004 and ended in July 2008.

Researchers

• Dr. Michael Backes
• Prof. Dr. David Basin
• Prof. Dr. Birgit Pfitzmann
• Dr. Christoph Sprenger
• Dr. Michael Waidner

News

• Nov 13, 2008: major reorganization and update of this web page, including update of browsable Isabelle/HOL theories to the latest version.
  

Contents

1. Background and Motiviation
2. Objectives and Approach
3. Contribution I. Monadic Modeling and Verification Tools
4. Contribution II. Two Formalizations of the BPW Model
5. Contribution III. Abstract Protocol Model
6. Summary and Conclusions
7. Publications & Further Information
8. Isabelle/HOL Source Code

Background and Motivation

Computational security definitions are formulated in terms of a probabilistic polynomial-time attacker having a negligible probability of success to break a given protocol or primitive. Cryptographers typically reduce protocol security proofs to the security of the underlying cryptographic primitives. Such proofs are often long, difficult and prone to human errors due to the lack of tool assistance. On the other hand, tools do exist for protocol verification in symbolic Dolev-Yao models. However, since these models abstract completely from computational issues and assume that cryptography is perfect (i.e., unbreakable), they usually lack a rigorous cryptographic justification. We aim at combining the best of both worlds: tool-supported symbolic proofs with strong cryptographic guarantees.

The Backes-Pfitzmann-Waidner Model

Backes, Pfitzmann, and Waidner were the first to propose a symbolic Dolev-Yao-style model (the BPW model) in the form of a  library of cryptographic primitives, which is cryptographically faithful with respect to its cryptographic realization in the sense of blackbox reactive simulatability (BRSIM). This means that there is a simulator that translates every probabilistic polynomial-time attacker of the cryptographic realization into an attacker of the BPW model such that honest users cannot distinguish the cryptographic from the symbolic setup. Moreover, BRSIM is compositional, i.e., preserved in all contexts, and preserves many security properties  from the symbolic to the cryptographic level. Hence, we may verify protocol security properties on the basis of the BPW model and conclude that they also hold for the cryptographic realization. To obtain cryptographic soundness the BPW model slightly deviates from standard Dolev-Yao models. For instance, it reflects the facts that secure encryption is probabilistic and often reveals the length of cleartexts.

Objectives and Approach

The main objective of this project is to enable machine-supported cryptographically sound reasoning about security protocols. This includes the formalization of protocol models in mathematical logic and the setup of an appropriate reasoning infrastructure. For maximum flexibility, we have chosen to work with a higher-order logic theorem prover, more specifically Isabelle/HOL. We  soon realized that in order to achieve a sufficient degree of proof automation we needed to abstract and simplify the BPW model. The project consisted of two phases. In the first phase, we modeled and abstracted the BPW model in Isabelle/HOL. In the second phase, we produced a more abstract protocol model, which is not based on the BPW model, but still cryptographically sound with respect to the BPW-based protocol model.

Note that at the end of each section below you find links to browsable versions of the corresponding Isabelle/HOL theories.

Contribution I. Monadic Modeling and Verification Tools

For modeling and reasoning about state-based systems in Isabelle/HOL, we built a generic monad-based modeling and verification toolbox [TPHOLs 2007]. We work with a simple component model, where a component is viewed as a state manipulated by a set of deterministic interface functions.  Components are implemented using a monad to model state and exceptions in the purely functional setting of Isabelle/HOL.  Components communicate using function calls. On the logical side, our toolbox includes a weakest pre-condition calculus and a monadic Hoare logic for pre-/post-condition reasoning, a linear-time temporal logic for temporal properties and a novel relational Hoare logic for proving the bisimilarity of monadic components. Using these tools we formalized all concepts and proofs described below in Isabelle/HOL.

Isabelle/HOL theories browser

• monadic modeling and verification toolbox (click here)
  

Contribution II. Two Formalizations of the BPW Model

In the first phase [CSFW 2006], we  produced two formalizations of the BPW model in Isabelle/HOL, which incrementally abstract the original account by Backes, Pfitzmann, and Waidner. The first formalization abstracts the component and communication model and the second one abstracts the message representation from a pointer-like structure to an inductively defined data type. We used our relational Hoare logic to prove that the two formalizations are bisimilar (and hence BRSIM), which allows us to work with the more abstract one for protocol verification. These two abstraction steps are both necessary for effective practical protocol verification work.

We validated our model by proving the security of the Needham-Schroeder-Lowe (NSL) protocol. Although the proof was feasible using our monadic Hoare logic and the weakest pre-condition calculus, it was very long (130 pages of Isabelle/HOL) and tedious. We have identified two main shortcomings that impede efficient specification and reasoning about protocols. First, there is no support for concise protocol specifications. Instead, each protocol needs to be defined from scratch using the fine-grained message manipulation operations of the BPW model. Second, these operations have side-effects, which complicates the proof of general results that are reusable in different protocol proofs. Moreover, the indirect reference to messages using handles in the BPW model constitutes an additional complexity. As a result our proof of the NSL protocol is around two orders of magnitude larger than Paulson's proof (which he did in a much simpler model).

Isabelle/HOL theories browser

• second formalization of BPW model (click here)
• first formalization and proof of bisimulation with second one (click here)
  
• generic protocol model and Needham-Schroeder-Lowe protocol (click here)

Contribution III. Abstract Protocol Model

In the second phase [CSF 2008/LICS 2008], we addressed these problems by a further abstraction step: We introduced concise role-based protocol specifications interpreted within a more abstract protocol model. More precisely, we defined a generic protocol interpreter for role-based specifications. Protocol roles consist of a sequence of pairs of input and output patterns. A protocol step corresponds to matching an incoming message against the input pattern and producing a reply message according to the output pattern. We produced two instantiations of the generic protocol interpreter, which differ by the implementation of pattern matching and message composition. In the first one, the concrete protocol model, these operations are based on the fined-grained BPW model operations (where messages are handles) and in the second one, the abstract protocol model, these operations are side-effect-free and directly manipulate message terms. We also substantially simplified the adversary by collapsing the 20+ BPW model adversary interface functions into a single abstract one, which checks the derivability of the messages the adversary intends to send. This test is based on side-effect-free, standard Dolev-Yao closure operations to analyze known and synthesize new messages.

To show the correctness of this abstraction step in the sense of BRSIM, we needed to (1) define a simulator mapping the concrete to the abstract adversary; the simulator essentially consists of the adversary part of the BPW model and maps handles to messages and vice versa, and (2) prove that, for each role-based protocol specification p, the concrete model instantiated to p is bisimilar to the composition of the simulator with the abstract model instantiated to p. The BRSIM proof is based on our relational Hoare logic and relies on several auxiliary invariants, mainly regarding the well-formedness of the protocol threads. It allows us to transfer security properties from the abstract protocol model to the concrete one that is based on the BPW model.

Reasoning about protocols in the abstract model

To reason about protocols within the abstract protocol model, we have developed a general proof infrastructure and technique (applicable to all role-based protocol specifications) to reduce the proof of each invariant to two core lemmas: one for the protocol steps, stating that the addition of a protocol message to the execution trace preserves the invariant, and one for the adversary, stating invariant preservation for messages derived by the adversary. This reduction is completely straightforward and can very likely be automated. To prove the user-side core lemma, we use two kinds of general results. First, we have proved a general logical characterization of generic protocol steps in Hoare logic. Second, for each protocol under study, we systematically state and prove a case analysis lemma, which specializes a generic protocol step to those of the given protocol. The proof of the adversary side core lemma is simplified by the fact that message derivation by adversary is based on side-effect-free standard operators to synthesize and analyse messages. Thus, we can use standard results about these operators. These core lemmas correspond very closely to the inductive steps in Paulson's method. Using this infrastructure, we have validated our expectation to obtain much simpler and shorter proofs by verifying the security of the NSL protocol within the abstract protocol model. Although the overall proof is still large (80 pages of Isabelle/HOL), the proofs of core lemmas for the 9 NSL invariants fit on around 10 pages.

Isabelle/HOL theories browser

• abstract protocol model, the proof of BRSIM/UC with the concrete interpretation based on the BPW model and a proof of the Needham-Schroeder-Lowe protocol  (click here)

Summary and Conclusions

In summary, the chosen abstractions close the gap with standard symbolic models both with respect to the conciseness of protocol and property specifications and the size and complexity of the resulting proofs. The benefits of these abstractions are two-fold:

• conceptually, they improve our understanding of the BPW model by relating it to more standard symbolic protocol models, and
  
• practically, they have allowed us to achieve the main objective of this project, namely, to provide efficient machine assistance for cryptographically sound reasoning about security protocols.
  

The complete project, with a particular emphasis on the second phase, is described in our CSF/LICS 2008 paper.

Publications & Further Information

• Christoph Sprenger and David Basin, Cryptographically-sound Protocol-model Abstractions, in Proceedings of Computer Security Foundations (CSF '08), IEEE Computer Society, 2008.
  

• Christoph Sprenger and David Basin, Cryptographically-sound Protocol-model Abstractions, in Proceedings of Logic in Computer Science (LICS '08), IEEE Computer Society, 2008.
  

• Christoph Sprenger and David Basin, A monad-based modeling and verification toolbox with application to security protocols, to appear in Theorem Proving in Higher-Order Logics (TPHOLs), Lecture Notes in Computer Science, vol. 4732, pp. 301-317, Springer-Verlag, 2007

• Christoph Sprenger, Michael Backes, David Basin, Birgit Pfitzmann and Michael Waidner, Cryptographically Sound Theorem Proving, In Proceedings of Computer Security Foundations Workshop, CSFW06, Venice, pp. 153-166, July 2006.
  
  A slightly older version is available as Cryptology ePrint Archive Report 2006/047.

For further information about this project you may also want to visit this page at IBM research, or directly contact one of the project members by following the respective link on the top of this page.

Isabelle/HOL Source Code

The source code of our development can be downloaded by clicking on the link below. You need a working installation of Isabelle/HOL 2005.

• CryptoProtocols-v0.8-060831.tgz

Note: This source distribution does not yet include the abstract protocol model, for which currently only the browsable documentation is available (see above).  A release of the complete sources is planned shortly (as of Nov 2008).

Please send mail to Christoph Sprenger if you would like to be notified of updates.