| Acronym: ComFormCrypt |
| Main Objective: This project addresses the problem of correct symbolic abstractions of cryptographic primitives for the purpose of symbolic, automated proving of security properties of protocols. 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. Computational soundness of formal cryptography is an active research area and members of this team have been involved in several of its fronts [ABS05,ABHS05,ABHS09,AF06,AFGZN08,BHO07,BHO09,BMS06] 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. So far in the literature there are fragmented attempts done by different research groups, but as their treatment lack sound mathematical basis, the results themselves and how they are related are questionable [AR02,ABHS09,AF06,BPW03,C01,CC08,DDMST05,MW04] We expect this research project to deliver new insights to the relationship between the symbolic and computational models, clarify the applicability and limitations of 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 of this research 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 |
| Reference: PTDC/EIA-CCO/113033/2009 |
| Funding: FCT/PTDC |
| Start Date: 01-02-2011 |
| End Date: 01-07-2014 |
| Team: Pedro Miguel dos Santos Alves Madeira Adão, Gergely István Bana, Carlos Manuel Costa Lourenco Caleiro, Paulo Alexandre Carreira Mateus, Pedro Alexandre Cardoso Baltazar, David Henriques, Andreia Filipa Torcato Mordido, Filipe Manuel Rodrigues Casal |
| Groups: Security and Quantum Information - Lx |
| Partners: |
| Local Coordinator: Pedro Miguel dos Santos Alves Madeira Adão |
| Links:
http://www.math.ist.utl.pt/~padao/projects/ComFormCrypt/index.html Internal Page |
|
|
|
Associated Publications
|
