Introduction

Modeling cryptographic protocols and analyzing their security is a tricky business. On the one hand, valid modeling and analysis has to address the concurrency aspects of asynchronous distributed systems, with potentially adversarial scheduling of events. On the other hand, realistic analysis has to accommodate the fact that, in most interesting cases, it is impossible to completely prevent successful attacks against the protocol. Instead, we can only bound the success probability of attacks that use a bounded amount of computational resources, based on underlying computational hardness assumptions.

Cryptographic modeling and analysis is typically complex, involving many subtleties and details, even when the analyzed protocols are simple. Furthermore, analysis is handwritten and often tedious to verify. These factors make security analysis of cryptographic protocols susceptible to errors and omissions.

This project demonstrates how to cast cryptographic security analysis of distributed protocols within the Probabilistic I/O Automata framework of Lynch, Segala, and Vaandrager [1]. This framework provides standard tools for arguing rigorously about the concurrency and scheduling aspects of protocols. It supports reasoning with multiple levels of abstraction and has a well-defined notion of composition. Consequently, using the PIOA framework can help in making cryptographic analysis more precise and less susceptible to errors.

In the context of this project, we aim to develop general techniques applicable to the analysis of a wide range of security protocols that exhibit various levels of complexity in terms of adversarial behavior or the use of cryptographic primitives. As a first step, we are currently analyzing a relatively simple protocol, two-party Oblivious Transfer protocol, in the presence of a semi-honest adversary (essentially, an eavesdropper). The particular OT protocol we analyze is the classic protocol of [2], which uses trapdoor permutations (and hard-core predicates for them) as the underlying cryptographic primitive. For the underlying cryptographic notion of security, we start from Canetti's Universally Composable Security [3].

In spite of the relative simplicity of the investigated case, the exercise is nontrivial and requires addressing fundamental issues such as modeling resource bounded-computations, resource-bounded adversarial behavior and scheduling, combining nondeterministic and probabilistic choices, and modeling computational hardness assumptions some of which are beyond the reach of the existing semantic theory of probabilistic I/O automata. Therefore, this project involves not only using the probabilistic I/O automata of [1] in security protocol analysis but also extending the basic theory to address the requirements of such analysis.

Approach

One common approach to simplifying cryptographic protocol analysis and improving its correctness is to model cryptographic primitives as ``symbolic operations'', or ``ideal boxes'', which represent the security properties of the primitives in an idealized way that involves no error probabilities or computational issues. This approach is quite promising; however, it does not completely remove the need for cryptographic analysis of protocols. Rather, it only proves security of the overall protocol assuming security of the cryptographic primitives in use. One still has to prove security of these primitives in a full-fledged cryptographic model with all its subtleties. Our project proposes an alternative (in fact, complementary) approach to making cryptographic protocol analysis more systematic and rigorous, and thus less susceptible to errors.

We benefit from the powerful proof techniques that have traditionally been used within I/O automaton frameworks. In particular, we express the system at multiple levels of abstraction where the highest level in the abstraction hierarchy represents the specification of the protocol and the lowest level represents the real-world system running the protocol. We demonstrate simulation relations between these levels that allow us to conclude that the real-world system implements the abstract specification. The composition operation for PIOAs makes it possible to separate the specification of correctness and security requirements of the protocol, and to express the real-world system naturally, as a composition of logically separate units interacting with another.

Progress

We have successfully modeled the protocol using probabilistic I/O automata of [1] and have layed out our method for analysis. We have also specified the automata that appear in intermediate levels of abstraction in showing that the given protocol securely-realizes its specification in the sense of [3]. The cryptographic primitives are used only at these intermediate levels so that reasoning about resource-bounded computations and computational hardness assumptions can be isolated to those cases of the proof that involve these intermediate levels.

We have defined a special class of PIOAs, called task-PIOAs, that admit a simple scheduling mechanism and new notions of implementation relations and simulation relations for task-PIOAs that make our analysis more manageable. Furthermore, we extended our new theory to capture time-bounded computations and scheduling.

We are in the process of proving the implementation relationships between levels in our automaton hierarchy, using the appropriate notions of simulation relations and invariants, and composition theorems.

Future Work

We would like to assess the techniques we have developed so far in the analysis of more complex protocols. This complexity may be due more powerful adversaries, more complex interaction patterns between the components of the protocol, or more subtle uses of cryptographic primitives.

One limitation of our current approach is that the existing scheduling mechanism is oblivious to execution histories and, hence, limits the capabilities of the adversarial components significantly. We will investigate how our assumptions about task-PIOAs and scheduling mechanisms can be relaxed to enable the analysis of a larger class of protocols.

Once our modeling and proof techniques become more general and established, we can focus on mechanizing our proofs with interactive theorem-provers, or even automating some or all proof steps.

Research Support

This project is supported by DARPA Air Force contract number FA9550-04-C-0084, DARPA Award number F33615-01-C-1896, NSF Award numbers CCR-0326277 and CCR-0121277, NSF-Texas Engineering Experiment Station grant 64961-CS, DARPA/AFOSR MURI Award F49620-02-1-0325 and MURI AFOSR Award Number SA2796PO 1-0000243658.

References

[1] Nancy Lynch, Roberto Segala, and Frits Vaandrager. Compositionality for Probabilistic Automata. In Roberto Amadio and Denis Lugiez, editors, CONCUR 2003 - Concurrency Theory (14th International Conference on Concurrency Theory, Marseille, France, September, 2003) , volume 2761 of Lecture Notes in Computer Science, pages 208-221, Springer-Verlag, 2003. Also, long version to appear as Technical Report MIT-LCS-TR-907, MIT Laboratory for Computer Science, Cambridge, MA 02139.

[2] S. Even, O. Goldreich and A. Lempel, A randomized protocol for signing contracts, CACM vol. 28, No. 6, 1985, pp. 637-647.

[3] Ran Canetti. Universally composable security: A new paradigm for cryptographic protocols. Available at http://eprint.iacr.org/2000/067. Extended abstract in 42nd FOCS, 2001.