Using Probabilistic I/O Automata to Improve the Analysis of Cryptographic Protocols
by Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Olivier Pereira and Roberto Segala
Modelling cryptographic protocols and analysing their security is a tricky business. On the one hand, valid modelling and analysis must address the concurrency aspects of asynchronous distributed systems, with potentially adversarial scheduling of events. On the other hand, realistic analysis must 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 modelling and analysis is typically complex, involving many subtleties and details, even when the analysed protocols are simple. Furthermore, analysis is handwritten and often tedious to verify. These factors make the 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 (PIOA) framework of Lynch, Segala and Vaandrager. 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 analysing a relatively simple protocol, the two-party Oblivious Transfer (OT) protocol, in the presence of a semi-honest adversary (essentially, an eavesdropper). The particular OT protocol we are studying is the classic protocol by Even, Goldreich and Lempel, 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.
In spite of the relative simplicity of the investigated case, the exercise is non-trivial and requires addressing a number of fundamental issues. These include modelling resource-bounded computations, resource-bounded adversarial behaviour and scheduling, combining non-deterministic and probabilistic choices, and modelling computational hardness assumptions. Some of these are beyond the reach of the existing semantic theory of probabilistic I/O automata. This project therefore involves using not only probabilistic I/O automata 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 the security of the overall protocol by assuming the security of the cryptographic primitives in use. One still has to prove the security of these primitives in a fully 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 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.
Future Work
We would like to assess the techniques we have developed so far in the analysis of more complex protocols. This complexity arise through 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 significantly limits the capabilities of the adversarial components. 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 modelling and proof techniques become more general and established, we can focus on mechanizing our proofs with interactive theorem-provers, or even automate some or all of the proof steps.
Link:
Technical report: http://www.lcs.mit.edu/specpub.php?id=1792
Please contact:
Olivier Pereira, Université catholique de Louvain (FNRS), Belgium
Tel: +32 10 47 91 63
E-mail: pereira
dice.ucl.ac.be
