ComFormCrypt - Computational Semantics of Formal Methods in Cryptography

A project of  SQIG at  IT, funded by FCT PTDC/EIA-CCO/113033/2009 (February 1, 2011 - July 31, 2014).

Goal: Correct symbolic abstractions of cryptographic primitives in order to achieve reliable automated proofs of security protocols.

Description: Computer security has been of major interest in the past two decades. This field provides both interesting research problems and important applications to everyone's life such as e-commerce and e-government, hence the need for designing better and safer security protocols. Proving security of protocols however is a difficult task that sometimes cannot be performed by hand, therefore several tools have been designed to deal with such a complex problem [B01,BMV05,P98]. But the need for such (automated) tools is not only due to the complexity of the protocols. If we consider the simple protocol proposed by Needham and Schroeder in 1978 [NS78], it was not until 1996 that Lowe discovered his famous attack on the protocol using the CSP-model checker FDR [L96] and suggested a fix. The attack used a flaw in the protocol design, the encryption itself was assumed to be perfectly secure. With this "perfect" cryptography assumption the protocol is simple enough to be easily analyzed by standard model-checkers and theorem provers. The fix was shown to be safe as long as encryption was perfect.

But what happens when the cryptographic primitives are not perfect, which is the case in real life where we can always guess a key with small probability? After some positive results regarding cryptographic soundness of such abstractions, Warinschi [W03] showed that the same attack discovered by Lowe against the NS protocol, could be performed against the corrected version if a somewhat weak but standard encryption scheme is used, the El-Gamal encryption scheme. This result turned the attention of the research community for the need of soundness results for formal cryptography, ie, the importance to characterize when protocols proved correct using perfect cryptography are correct when implemented with computational cryptography.

Symbolic models provide abstractions for the study of cryptography that are amenable for automatic verification of complex protocols but assume "perfect cryptography" [DY93]. Messages, keys, encryptions, attacks, all appear as formal objects described with symbolic operations, axioms, derivation rules; cryptographic operations are modeled as functions on a space of symbolic expressions and security properties are also treated symbolically. This method ignores the probabilistic nature of encryptions. It provides a powerful way to describe how an adversary may interfere, corrupt, deceive participants of a protocol, and grab this way information not addressed to him. This method is much easier to handle mathematically than the computational, the proofs can be automated but, as the probabilistic nature is ignored, security within this framework does not necessarily mean security in the real world. Real probabilistic attacks that are outside the framework of this model may still happen [W03].

On the other hand in the computational model cryptographic operations act on strings of bit and their security properties are defined in terms of probability and computational complexity [GM84]. Computational security proofs make use of techniques of these theories; proofs have to be done by hand (ie cannot be automated) and are different for each protocol. Good protocols are those in which attackers cannot do something bad too often and efficiently enough. This is a very detailed description, closer to reality as it involves the notion of efficient computation, hence complexity and probabilities. However, even for mildly complex protocols this approach simply becomes too difficult and impossible to handle.

The unification of these two models is absolutely necessary for symbolic security proofs to be trustable. The aim of this research project is to deliver new insights on the relationship between the symbolic and computational models, clarify the applicability and limitations of the existing approaches to this problem, and provide sound mathematical foundations that can be used in the future as a common framework and technique for sound symbolic abstraction of new cryptographic primitives. The ultimate goal is to develop/adapt fully automated tools for symbolic models that, via our soundness results, entail strong cryptographic guarantees to the computational model, hence substituting the tedious complexity-theoretic proofs of computational cryptography by automated ones.

The main task of the project aims at developing a computationally sound logic to prove security properties. For further information contact Pedro Adão (project coordinator).

Team

Former Members

Publications:

Using SQIG website.

References:




Last update: September 1, 2014