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).
David Basin, Carlos Caleiro, Jaime Ramos, and Luca Vigano
Distributed Temporal Logic for the Analysis of Security Protocol Models
Theoretical Computer Science, 412(31):4007-4043, 2011.
© Elsevier.
Bruno Conchinha, David A. Basin, and Carlos Caleiro
FAST: An Efficient Decision Procedure for Deduction and Static Equivalence
In Manfred Schmidt-Schauss, editor,
22nd International Conference on Rewriting Techniques and Applications (RTA'11),
volume 10 of LIPIcs, pages 11-20,
Novi Sad, Serbia, May 30-June 1 2011.
© Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
Gergei Bana and Hubert Comon-Lundh
Towards Unconditional Soundness: Computationally Complete Symbolic Attacker
In Pierpaolo Degano and Joshua D. Guttman, editors,
1st International Conference on Principles of Security and Trust (POST'12),
volume 7215 of LNCS, pages 189-208,
Tallinn, Estonia, March 24-April 1 2012.
© Springer.
Gergei Bana, Pedro Adão, and Hideki Sakurada
Computationally Sound Verification of the NSL Protocol via Computationally Complete Symbolic Attacker
Presented at FCC'12. Affiliated Workshop of CSF'12, Harvard, CA, USA, June 27-28 2012.
Bruno Conchinha, David Basin, and Carlos Caleiro
Symbolic Probabilistic Analysis of Off-line Guessing
Presented at FCC'12. Affiliated Workshop of CSF'12, Harvard, CA, USA, June 27-28 2012.
Gergei Bana, Pedro Adão, and Hideki Sakurada
Computationally Complete Symbolic Attacker in Action
In Deepak D'Souza, Telikepalli Kavitha, and Jaikumar Radhakrishnan, editors,
32nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'12),
volume 18 of LIPIcs, pages 546-560,
Hyderabad, India, December 15-17 2012.
© Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
David Henriques, Manuel Biscaia, Pedro Baltazar, and Paulo Mateus
Decidability and Complexity for ω-regular Properties of Stochastic Systems
Logic Journal of IGPL, 20(6):1175-1201, December, 2012.
© Oxford University Press.
Pedro Baltazar, Luis Caires, Vasco T. Vasconcelos, and Hugo T. Vieira
A Type System for Flexible Role Assignment in Multiparty Communicating Systems
In Catuscia Palamidessi and Mark Dermot Ryan, editors,
7th International Symposium on Trustworthy Global Computing (TGC'12),
Affiliated Workshop of CONCUR'12,
volume 8191 of LNCS, pages 82-96,
Newcastle upon Tyne, UK, 7-8 September 2012.
© Springer.
João Mendes and Pedro Adão
Trusted Civitas: Client Trust in Civitas Electronic Voting Protocol
In Proceedings of INFORUM'12,
Caparica, Portugal, September 6-7 2012.
Francisco M. Assis, Aleksandar Stojanovic, Paulo Mateus, and Yasser Omar
Improving Classical Authentication over a Quantum Channel
Entropy, 14(12):2531-2549, 2012.
Gergei Bana, Koji Hasebe, and Mitsuhiro Okada
Computationally Complete Symbolic Attacker and Key Exchange
In Ahmad-Reza Sadeghi, Virgil D. Gligor, and Moti Yung, editor,
20th ACM Conference on Computer and Communications Security (CCS'13),
pages 1231-1246,
Berlin, Germany, November 4-8, 2013.
© ACM Press.
Pedro Adão and Carlos Caleiro
A Natural Deduction System for the Computational Complete Symbolic Adversary
Presented at FCC'13. Affiliated Workshop of MFPS-LICS-CSF'13, New Orleans, LA, USA, June 29 2013.
Bruno Conchinha, David A. Basin, and Carlos Caleiro
Symbolic Probabilistic Analysis of Off-Line Guessing
In Jason Crampton, Sushil Jajodia, and Keith Mayes, editors,
18th European Symposium on Research in Computer Security (ESORICS'13),
volume 8134 of LNCS, pages 363-380,
Egham, UK, September 9-13, 2013.
© Springer.
Pedro Adão, Paulo Mateus, and Luca Vigano
Protocol Insecurity with a Finite Number of Sessions and a Cost-Sensitive Guessing Intruder is NP-Complete
Theoretical Computer Science, 538:2-15, 2014.
© Elsevier.
Pedro Adão, Riccardo Focardi, and Flaminia L. Luccio
Type-Based Analysis of Generic Key Management APIs
In
Proceedings of the 26th IEEE Computer Security Foundations Symposium (CSF'13),
pages 97-111,
New Orleans, LA, USA, June 26-28, 2013.
© IEEE Computer Society.
Manuel Biscaia, Pedro Baltazar, Paulo Mateus, and Rajagopal Nagarajan
A Temporal Logic for Planning under Uncertainty
In Chutima Boonthum-Denecke and G. Michael Youngblood, editors,
26th International Florida AI Research Symposium (FLAIRS'13),
St. Pete Beach, Florida, USA, May 22-24, 2013.
© AAAI Press.
Alexandra M. Carvalho, Pedro Adão, and Paulo Mateus
Efficient Approximation of the Conditional Relative Entropy with Applications to Discriminative Learning of Bayesian Network Classifiers
Entropy, 15(7):2716-2735, 2013.
Gergei Bana and Hubert Comon-Lundh
A Computationally Complete Symbolic Attacker for Equivalence Properties
To appear in
21st ACM Conference on Computer and Communications Security (CCS'14),
Scottsdale, Arizona, USA, November 3-7, 2014.
© ACM Press.
Pedro Adão, Claudio Bozzato, Gian-Luca Dei Rossi, Riccardo Focardi, and Flaminia L. Luccio
A Semantic Based Tool for Firewall Configuration (Extended Abstract)
Presented at HotSpot'14. Affiliated Workshop of ETAPS'14, Grenoble, France, April 5 2014.
Pedro Adão, Claudio Bozzato, Gian-Luca Dei Rossi, Riccardo Focardi, and Flaminia L. Luccio
Mignis: A Semantic Based Tool for Firewall Configuration
In
Proceedings of the 27th IEEE Computer Security Foundations Symposium (CSF'14),
pages 351-365,
Vienna, Austria, July 19-22, 2014.
© IEEE Computer Society.
Alexandra M. Carvalho, Pedro Adão, and Paulo Mateus
Hybrid Learning of Bayesian Multinets for Binary Classification
Pattern Recognition, 47(10):3438-3450, 2014.
© Elsevier.
João Miguel Barros da Silva Mendes
Trusted Civitas: Client Trust in CIVITAS Electronic Voting Protocol
MSc in Information Systems and Computer Engineering. IST. May 2011. Supervised by Pedro Adão.
Andreia Filipa Torcato Mordido
Dynamic Probabilistic Epistemic Logic: Towards Information Security
MSc in Mathematics and Applications. IST. December 2011. Supervised by Carlos Caleiro.
Manuel Nunes Farinha Correia Rego
Security and Privacy in Identification and Mobile Payments
MSc in Information Systems and Computer Engineering. IST. October 29 2012. Supervised by Pedro Adão.