For timely ZISC-related information, you are kindly invited to subscribe to the ZISC Announcements Mailing List.
This project started in February 2004 and ended in July 2008.
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.
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.
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.
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.
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).
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.
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.
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:
The complete project, with a particular emphasis on the second phase, is described in our CSF/LICS 2008 paper.
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.
The source code of our development can be downloaded by clicking on the link below. You need a working installation of Isabelle/HOL 2005.
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.
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.