Pascal Lafourcade Publications

Magazine

[PPS08+]

Panos Papadimitratos, Marcin Poturalski, Patrick Schaller, Pascal Lafourcade, David Basin, Srdjan Capkun, Jean-Pierre Hubaux. Secure Neighborhood Discovery: A Fundamental Element for Mobile Ad Hoc Networking accepted for publication in IEEE Communications Magazine, 2008 PDF

Journal

[CDELL11] Judicael Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech: Automated Proofs for Asymmetric Encryption. J. Autom. Reasoning 46(3-4): 261-291 (2011). PDF | Bibtex | Abstract

@inproceedings{CDELL11-JAR,
author = {Judica{\"e}l Courant and Marion Daubignard and Cristian Ene and Pascal Lafourcade and Yassine Lakhnech},
title = {Automated Proofs for Asymmetric Encryption},
journal = {J. Autom. Reasoning},
volume = {46},
number = {3-4},
year = {2011},
pages = {261-291},
}

Many generic constructions for building secure cryptosystems from primitives with lower level of security have been proposed. Providing security proofs has also become standard practice. There is, however, a lack of automated verification procedures that analyze such cryptosystems and provide security proofs. In this paper, we present a sound and automated procedure that allows us to verify that a generic asymmetric encryption scheme is secure against chosen-plaintext attacks in the random oracle model. It has been applied to several examples of encryption schemes among which the construction of Bellare-Rogaway 1993, of Pointcheval at PKC'2000.

[CLN09] Cas Cremers, Pascal Lafourcade, and Philippe Nadeau. Comparing State Spaces in Automatic Protocol Analysis .Formal to Practical Security, LNCS, volume 5458/2009, 2009. PDF | PS | Bibtex | Abstract

@inproceedings{CLN2009comparing,
author = {Cas J.F. Cremers and Pascal Lafourcade and Philippe Nadeau},
title = {Comparing State Spaces in Automatic Protocol Analysis},
booktitle = {Formal to Practical Security},
Series = {Lecture Notes in Computer Science},
Publisher = {Springer Berlin / Heidelberg},
year = {2009},
volume = {5458/2009},
pages = {70-94},
}

There are several automatic tools available for the symbolic analysis of security protocols. The models underlying these tools differ in many asp ects. Some of the differences have already been formally related to each other in the literature, such as diference in protocol execution models or definitions of security properties. However, there is an important difference between analysis tools that has not b een investigated in depth before: the explored state space. Some tools explore all possible behaviors, whereas others explore strict subsets, often by using so-called scenarios. We identify several typ es of state space explored by protocol analysis tools, and relate them to each other. We find previously unreported dif- ferences between the various approaches. Using combinatorial results, we determine the requirements for emulating one typ e of state space by combinations of another type. We apply our study of state space relations in a p erformance compari- son of several well-known automatic tools for security protocol analysis. We model a set of protocols and their prop erties as homogeneously as possible for each tool. We analyze the p erformance of the tools over comparable state spaces. This work enables us to effectively compare these automatic tools, i. e., using the same protocol description and exploring the same state space. We also prop ose some explanations for our exp erimental results, leading to a b etter understanding of the tools.

[DLLT08] Stéphanie Delaune, Pascal Lafourcade, Denis Lugiez and Ralf Treinen. Symbolic protocol analysis for monoidal equational theories. Information and Computation, 2008. PDF | Bibtex | Abstract

@article{DLLT-IC07,
author = {Delaune, St{\'e}phanie and Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
DOI = {10.1016/j.ic.2007.07.005},
journal = {Information and Computation},
volume ={206},
pages = {312-351},
month = feb # {-} # apr,
publisher = {Elsevier Science Publishers},
title = {Symbolic protocol analysis for monoidal equational theories},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLLT-ic07.pdf},
year = {2008},
}

We are interested in the design of automated procedures for analyzing the (in)security of cryptographic protocols in the Dolev-Yao model for a bounded number of sessions when we take into account some algebraic properties satisfied by the operators involved in the protocol. This leads to a more realistic model than what we get under the perfect cryptography assumption, but it implies that protocol analysis deals with terms modulo some equational theory instead of terms in a free algebra. The main goal of this paper is to set up a general approach that works for a whole class of monoidal theories which contains many of the specific cases that have been considered so far in an ad-hoc way (e.g. exclusive or, Abelian groups, exclusive or in combination with the homomorphism axiom). We follow a classical schema for cryptographic protocol analysis which proves first a locality result and then reduces the insecurity problem to a symbolic constraint solving problem. This approach strongly relies on the correspondence between a monoidal theory E and a semiring SE which we use to deal with the symbolic constraints. We show that the well-defined symbolic constraints that are generated by reasonable protocols can be solved provided that unification in the monoidal theory satisfies some additional properties. The resolution process boils down to solving particular quadratic Diophantine equations that are reduced to linear Diophantine equations, thanks to linear algebra results and the well-definedness of the problem. Examples of theories that do not satisfy our additional properties appear to be undecidable, which suggests that our characterization is reasonably tight.

[LLT07] Pascal Lafourcade, Denis Lugiez and Ralf Treinen. Intruder Deduction for the Equational Theory of Abelian Groups with Distributive Encryption. Information and Computation 205(4), pages 581-623, 2007. PDF | PS | PS.GZ | Bibtex | Abstract

Cryptographic protocols are small programs which involve a high level of concurrency and which are difficult to analyze by hand. The most successful methods to verify such protocols are based on rewriting techniques and automated deduction in order to implement or mimic the process calculus describing the execution of a protocol. We are interested in the intruder deduction problem, that is vulnerability to passive attacks in presence of equational theories which model the protocol specification and properties of the cryptographic operators.
In the present paper we consider the case where the encryption distributes over the operator of an Abelian group or over an exclusive-or operator. We prove decidability of the intruder deduction problem in both cases. We obtain a PTIME decision procedure in a restricted case, the so-called binary case.
These decision procedures are based on a careful analysis of the proof system modeling the deductive power of the intruder, taking into account the algebraic properties of the equational theories under consideration. The analysis of the deduction rules interacting with the equational theory relies on the manipulation of Z-modules in the general case, and on results from prefix rewriting in the binary case.

@article{LLT-icomp07,
author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
DOI = {10.1016/j.ic.2006.10.008},
journal = {Information and Computation},
month = apr,
number = {4},
pages = {581-623},
publisher = {Elsevier Science Publishers},
title = {Intruder Deduction for the Equational Theory of {A}belian Groups with Distributive Encryption},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LLT-icomp07.pdf},
volume = {205},
year = {2007},
}

[CDL06] Véronique Cortier, Stéphanie Delaune and Pascal Lafourcade. A Survey of Algebraic Properties Used in Cryptographic Protocols. Journal of Computer Security 14(1), pages 1-43, 2006. PDF | PS| PS.GZ | Bibtex | Abstract

Cryptographic protocols are successfully analyzed using formal methods. However, formal approaches usually consider the encryption schemes as black boxes and assume that an adversary cannot learn anything from an encrypted message except if he has the key. Such an assumption is too strong in general since some attacks exploit in a clever way the interaction between protocol rules and properties of cryptographic operators. Moreover, the executability of some protocols relies explicitly on some algebraic properties of cryptographic primitives such as commutative encryption. We give a list of some relevant algebraic properties of cryptographic operators, and for each of them, we provide examples of protocols or attacks using these properties. We also give an overview of the existing methods in formal approaches for analyzing cryptographic protocols.

@article{CDL05-survey,
author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie and Lafourcade, Pascal},
journal = {Journal of Computer Security},
number = {1},
pages = {1-43},
publisher = {{IOS} Press},
title = {A Survey of Algebraic Properties Used in Cryptographic Protocols},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/surveyCDL.pdf},
volume = {14},
year = {2006},
}

Conferences

[FLA11] Fousse, Laurent and Lafourcade, Pascal and Alnuaimi, Mohamed: Benaloh's Dense Probabilistic Encryption Revisited. In Progress in Cryptology - AFRICACRYPT 2011 - 4th International Conference on Cryptology in Africa, Dakar, Senegal, July 5-7, 2011. Proceedings, 2011. PDF | Bibtex | Abstract | Slides

@inproceedings{FLA11,
title = {Benaloh's Dense Probabilistic Encryption Revisited },
author = {Fousse, Laurent and Lafourcade, Pascal and Alnuaimi, Mohamed},
year = {2011},
booktitle = {Progress in Cryptology - AFRICACRYPT 2011 - 4th International Conference on Cryptology in Africa, Dakar, Senegal, July 5-7, 2011. Proceedings},
pages = {348-362},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6737},
team = {DCS},
}

In 1994, Josh Benaloh proposed a probabilistic homomor- phic encryption scheme, enhancing the poor expansion factor provided by Goldwasser and Micali's scheme. Since then, numerous papers have taken advantage of Benaloh's homomorphic encryption function, including voting schemes, private multi-party trust computation, non-interactive verifiable secret sharing, online poker. In this paper we show that the original description of the scheme is incorrect, because it can result in ambiguous decryption of ciphertexts. Then we show on several applications that a bad choice in the key generation phase of Benaloh's scheme has a real impact on the behaviour of the application. For instance in an e-voting protocol, it can inverse the result of an election. Our main contribution is a corrected description of the scheme (we provide a complete proof of correctness). Moreover we also compute the probability of failure of the original scheme. Finally we show how to formulate the security of the corrected scheme in a generic setting suitable for several homomorphic encryptions.

[ADLP11] Routage par marche aléatoire à listes tabous. Altisen, Karine and Devismes, Stéphane and Lafourcade, Pascal and Ponsonnet, Clément (in Algotel, 2011). PDF | Bibtex | Abstract

@inproceedings{ADL+11,
title = {Routage par marche al\\'eatoire \\`{a} listes tabous },
author = {Altisen, Karine and Devismes, St\\'ephane and Lafourcade, Pascal and Ponsonnet, Cl\\'ement},
year = {2011},
booktitle = {Algotel},
note = {to appear},
}

Nous proposons d'améliorer les marches aléatoires en utilisant des listes tabous. Notre objectif est de réduire le nombre de sauts pour atteindre un noeud particulier du réseau sans compromettre les autres avantages des marches aléatoires. Nos solutions permettent ainsi de résoudre efficacement le routage dans les réseaux de capteurs sans fil.

[DLL11] Jannik Dreier, Pascal Lafourcade, Yassine Lakhnech. Vote-Independence: A Powerful Privacy Notion for Voting Protocols. 4th Canada-France MITACS Workshop on Foundations & Practice of Security (FPS'11), 2011. PDF | Technical Report

[JWESML10] Jérémie Tharaud, Sven Wohlgemuth, Isao Echizen, Noboru Sonehara, Gunter Muller, Pascal Lafourcade: Privacy by Data Provenance with Digital Watermarking - A Proof-of-Concept Implementation for Medical Services with Electronic Health Records. IIH-MSP 2010: 510-513 PDF | Bibtex | Abstract

@inproceedings{TWE+10,
title = {Privacy by Data Provenance with Digital Watermarking - A Proof-of-Concept Implementation for Medical Services with Electronic Health Records },
author = {Tharaud, J{\\'e}r{\\'e}mie and Wohlgemuth, Sven and Echizen, Isao and Sonehara, Noboru and M{\"u}ller, G{\"u}nter and Lafourcade, Pascal},
year = {2010},
booktitle = {Sixth International Conference on Intelligent Information Hiding and Multimedia Signal Processing (IIH-MSP 2010), Darmstadt, Germany, 15-17 October, 2010, Proceedings},
pages = {510-513},
publisher = {IEEE Computer Society},
}

Security is one of the biggest concerns about Cloud Computing. Most issues are related to security problems faced by cloud providers, who have to ensure that their infrastructure is properly secure and client data are protected, and by the customers, who must ensure proper security measures have been taken by the provider in order to protect their personal data. When you move your information into the cloud, you lose control of it. The cloud gives you access to your data, but you have no way of ensuring no one else has access to these data. In this article, we propose an evaluation of a proof-of-concept implementation of a usage control system for an ex post enforcement of privacy rules regarding the disclosure of personal data to third parties. The system is based on cryptographic protocols and digital watermarking in medical services and electronic health records.

[GLLS09] Martin Gagné, Pascal Lafourcade, Yassine Lakhnech, and Reihaneh Safavi-Naini Automated Proofs for Encryption Modes. In Proceedings of the 13th Annual Asian Computing Science Conference Focusing on Information Security and Privacy: Theory and Practice (ASIAN'09),October 2009. PDF | PS | Bibtex|Abstract | Slides

@inproceedings{GLLS-ASIAN09,
author = {Martin Gagné, Pascal Lafourcade, Yassine Lakhnech, and Reihaneh Safavi-Naini},
booktitle = {13th Annual Asian Computing Science Conference Focusing on Information Security and Privacy: Theory and Practice (ASIAN'09)},
address = {Urumqi, China},
editor = { },
month = {oct},
pages = {},
title = {Automated Proofs for Encryption Modes},
year = {2009},
}

We presents a compositional Hoare logic for proving semantic security of modes of operation for symmetric key block ciphers. We propose a simple programming language to specify encryption modes and an assertion language that allows to state invariants and axioms and rules to establish such invariants. The assertion language consists of few atomic predicates. We were able to automatically verify semantic security of several encryption modes including Cipher Block Chaining (CBC), Cipher Feedback mode (CFB), Output Feedback (OFB), and Counter mode (CTR).

[CDELL08a] Judicael Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade. and Yassine Lakhnech Towards Automated Proofs for Asymmetric Encryption Schemes in the Random Oracle Model. In Proceedings of the 15th ACM Conference on Computer and Communications Security, (CCS'08), October 2008, Alexandria USA. Pdf | PS | Bibtex | Abstract

Chosen-ciphertext security is by now a standard security property for asymmetric encryption. Many generic constructions for building secure cryptosystems from primitives with lower level of security have been proposed. Providing security proofs has also become standard practice. There is, however, a lack of automated verification procedures that analyse such cryptosystems and provide security proofs. This paper presents an automated procedure for analysing generic asymmetric encryption schemes in the random oracle model. It has been applied to several examples of encryption schemes among which the construction of Bellare-Rogaway 1993, REACT and Pointcheval at PKC'2000.

@inproceedings{CDELL-CCS08,
title = {Towards Automated Proofs for Asymmetric Encryption Schemes in the Random Oracle Model},
author = {Judicael Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade. and Yassine Lakhnech},
booktitle = {{P}roceedings of the 15th ACM Conference on Computer and Communications Security, (CCS'08)},
editor = {Peng Ning and Paul F. Syverson and Somesh Jha},
month = {oct},
pages = {371-380},
publisher = {ACM},
year = {2008},
address = {Alexandria, USA},
}

[Laf07] Pascal Lafourcade. Intruder Deduction for the Equational Theory of Exclusive-or with Commutative and Distributive Encryption. In Maribel Fernández and Claude Kirchner (eds.), Proceedings of the 1st International Workshop on Security and Rewriting Techniques (SecReT'06), Venice, Italy, July 2006, Electronic Notes in Theoretical Computer Science 171(4), pages 37-57. Elsevier Science Publishers, 2007. PDF | PS| PS.GZ | Bibtex | Abstract

The first step in the verification of cryptographic protocols is to decide the intruder deduction problem, that is the vulnerability to a so-called passive attacker. We extend the Dolev-Yao model in order to model this problem in presence of the equational theory of a commutative encryption operator which distributes over the exclusive-or operator. The interaction between the commutative distributive law of the encryption and exclusive-or offers more possibilities to decrypt an encrypted message than in the non-commutative case, which imply a more careful analysis of the proof system. We prove decidability of the intruder deduction problem for a commutative encryption which distributes over exclusive-or with a DOUBLE-EXPTIME procedure. And we obtain that this problem is EXPSPACE-hard in the binary case.

@inproceedings{Laf-secret06,
address = {Venice, Italy},
author = {Lafourcade, Pascal},
booktitle = {{P}roceedings of the 1st {I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques ({SecReT}'06)},
DOI = {10.1016/j.entcs.2007.02.054},
editor = {Fern{\'a}ndez, Maribel and Kirchner, Claude},
month = jul,
number = {4},
pages = {37-57},
publisher = {Elsevier Science Publishers},
series = {Electronic Notes in Theoretical Computer Science},
title = {Intruder Deduction for the Equational Theory of {\emph{Exclusive-or}} with Commutative and Distributive Encryption},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Laf-secret06-long.pdf},
volume = {171},
year = {2007},
}

[DLLT06] Stéphanie Delaune, Pascal Lafourcade, Denis Lugiez and Ralf Treinen. Symbolic Protocol Analysis in Presence of a Homomorphism Operator and Exclusive Or. In Michele Buglesi, Bart Preneel, Vladimiro Sassone and Ingo Wegener (eds.), Proceedings of the 33rd International Colloquium on Automata, Languages and Programming (ICALP'06) - Part II, Venice, Italy, July 2006, Lecture Notes in Computer Science 4052, pages 132-143. Springer. PDF | PS| PS.GZ | PDF (long version) | PS(long version) | PS.GZ (long version) | Bibtex | Abstract

Security of a cryptographic protocol for a bounded number of sessions is usually expressed as a symbolic trace reachability problem. We show that symbolic trace reachability for well-defined protocols is decidable in presence of the exclusive or theory in combination with the homomorphism axiom. These theories allow us to model basic properties of important cryptographic operators. This trace reachability problem can be expressed as a system of symbolic deducibility constraints for a certain inference system describing the capabilities of the attacker. One main step of our proof consists in reducing deducibility constraints to constraints for deducibility in one step of the inference system. This constraint system, in turn, can be expressed as a system of quadratic equations of a particular form over Z/2Z[h], the ring of polynomials in one indeterminate over the finite field Z/2Z. We show that satisfiability of such systems is decidable.

@inproceedings{DLLT-ICALP2006,
address = {Venice, Italy},
author = {Delaune, St{\'e}phanie and Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
booktitle = {{P}roceedings of the 33rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'06)~--- {P}art~{II}},
DOI = {10.1007/11787006_12},
editor = {Buglesi, Michele and Preneel, Bart and Sassone, Vladimiro and Wegener, Ingo},
month = jul,
pages = {132-143},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Symbolic Protocol Analysis in Presence of a Homomorphism Operator and {\emph{Exclusive~Or}}},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DLLT-icalp06.pdf},
volume = {4052},
year = {2006},
}

[LLT05a] Pascal Lafourcade, Denis Lugiez and Ralf Treinen. Intruder Deduction for AC-like Equational Theories with Homomorphisms. In Juergen Giesl (ed.), Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA'05), Nara, Japan, April 2005, Lecture Notes in Computer Science 3467, pages 308-322. Springer. PDF | PS| PS.GZ | PS(long version) | PS.GZ (long version) | Bibtex | Abstract

Cryptographic protocols are small programs which involve a high level of concurrency and which are difficult to analyze by hand. The most successful methods to verify such protocols rely on rewriting techniques and automated deduction in order to implement or mimic the process calculus describing the protocol execution.
We focus on the intruder deduction problem, that is the vulnerability to passive attacks, in presence of several variants of AC-like axioms (from AC to Abelian groups, including the theory of exclusive or) and homomorphism which are the most frequent axioms arising in cryptographic protocols. Solutions are known for the cases of exclusive or, of Abelian groups, and of homomorphism alone. In this paper we address the combination of these AC-like theories with the law of homomorphism which leads to much more complex decision problems.
We prove decidability of the intruder deduction problem in all cases considered. Our decision procedure is in EXPTIME, except for a restricted case in which we have been able to get a PTIME decision procedure using a property of one-counter and pushdown automata.

@inproceedings{LLT-rta2005,
address = {Nara, Japan},
author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
booktitle = {{P}roceedings of the 16th {I}nternational {C}onference on {R}ewriting {T}echniques and {A}pplications ({RTA}'05)},
DOI = {10.1007/b135673},
editor = {Giesl, J{"u}rgen},
month = apr,
pages = {308-322},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Intruder Deduction for {AC}-like Equational Theories with Homomorphisms},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/rta05-LLT.pdf},
volume = {3467},
year = {2005},
}

Thesis

[Laf06] Pascal Lafourcade. Vérification des protocoles cryptographiques en présence de théories équationnelles. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, September 2006. 209 pages. PDF | PS| PS.GZ | Slides | Bibtex | Abstract

The rise of the internet of new technologies has reinforced the key role of computer science in communication technology. The recent progress in these technologies has brought a dramatic change in the ways how we communicate and consume. All these communication activities are subject to complex communication protocols that a user does not control completely. Users of communication protocols require that their communications are secure. The developers of these communication protocols aim to secure communications in a hostile environment by cryptographic means. Such an environment consists of a dishonest communication participant, called an intruder or attacker... We suppose that the intruder controls the network on which the messages are exchanged.
The verification of a cryptographic protocol either ensures that no attack is possible against the execution of the protocol in presence of a certain intruder, or otherwise exhibits an attack. One important assumption in the verification of cryptographic protocols is the so-called perfect cryptography assumption, which states that the only way to obtain knowledge about an encrypted message is to know its decryption key. This hypothesis is not sufficient to guarantee security in reality. It is possible that certain properties used in the protocol allow the intruder to obtain some information.
One way to weaken this perfect cryptography assumption is to take into account in the model certain algebraic properties. We develop a formal approach for verifying the so-called secrecy property of cryptographic protocols in the presence of equational theories and of homomorphism.

@phdthesis{THESE-lafourcade06,
author = {Lafourcade, Pascal},
month = sep,
note = {209~pages},
school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France},
type = {Th{\`e}se de doctorat},
title = {V{\'e}rification des protocoles cryptographiques en pr{\'e}sence de th{\'e}ories {\'e}quationnelles},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-lafourcade.pdf},
year = {2006},
}

Others

[LTV09] Pascal Lafourcade, Vanessa Terrade and Sylvain Vigier Comparison of Cryptographic Verification Tools Dealing with Algebraic Properties . In Proceedings of the sixth International Workshop on Formal Aspects in Security and Trust (FAST2009), November 2009, Eindhoven, the Netherlands. PDF | PS| Slide | Bibtex| Abstract

Recently Kuesters et al proposed two new methods using ProVerif for analyzing cryptographic protocols with XOR and Diffie Hellman properties. Some tools are able to deal with XOR and Diffie Hellman. In this article we compare time efficiency these tools. For this purpose we verify with these tools some protocols of the litterature that are designed with such algebraic properties.

@inproceedings{LTV09,
author = {Pascal Lafourcade, Vanessa Terrade and Sylvain Vigier},
booktitle = { sixth International Workshop on Formal Aspects in Security and Trust, (FAST'09)},
address = { Eindhoven, Netherlands},
editor = {Joshua Guttman, Pierpaolo Degano},
month = {nov},
pages = {},
title = { Comparison of Cryptographic Verification Tools Dealing with Algebraic Properties },
year = {2009},
}

[GLLS09] Martin Gagné, Pascal Lafourcade, Yassine Lakhnech, and Reihaneh Safavi-Naini Automated Proofs for Encryption Modes. In Proceedings of the Workshop on Formal and Computational Cryptography, (FCC'09), July 2009, PortJefferson NY, USA. PDF | PS | Bibtex| Abstract

We presents a compositional Hoare logic for proving semantic security of modes $ symmetric key block ciphers. We propose a simple programming language to specify encryption modes and an assertion language that allows to state invariants and axioms and rules to establish such invariants. The assertion language consists of few atomic predicates. We were able to use our method to verify semantic security of several encryption modes including Cipher Block Chaining (CBC), Cipher Feedback mode (CFB), Output Feedback (OFB), and Counter mode (CTR).

@inproceedings{GLLS-FCC09,
author = {Martin Gagné, Pascal Lafourcade, Yassine Lakhnech, and Reihaneh Safavi-Naini},
booktitle = {Workshop on Formal and Computational Cryptography, (FCC'09)},
address = {Port Jefferson NY, USA},
editor = {Ralf Kuesters},
month = {jul},
pages = {},
title = {Automated Proofs for Encryption Modes},
year = {2009},
}

[ML09] Sreekanth Malladi, Pascal Lafourcade, Prudent engineering practices to prevent type-flaw attacks under algebraic properties . In Proceedings of the Workshop on Security and Rewriting Techniques, (Secret'09) July 2009, PortJefferson NY, USA. PDF | PS | Bibtex| Abstract

We investigate type-flaw attacks on cryptographic protocols when messages possess algebraic properties such as associativity, commutativity and several others. We advocate some prudent engineering practices to prevent those attacks. Our most interesting contribution is proving that type-tagging prevents all type-flaw attacks under monoidal operators such as Exclusive-OR.

@inproceedings{ML-Secret09,
author = {Sreekanth Malladi and Pascal Lafourcade },
booktitle = {Workshop on Security and Rewriting Techniques, (SecReT'09)},
address = {Port Jefferson NY, USA},
editor = {Comon-Lundh, Hubert and Meadows, Catherine},
month = {jul},
pages = {},
title = {Prudent engineering practices to prevent type-flaw attacks under algebraic properties },
year = {2009},
}

[Laf08] Pascal Lafourcade. Relation between Unification Problem and Intruder Deduction Problem. In Proceedings of the 3rd International Workshop on Security and Rewriting Techniques (SecReT'08), Pittsburgh, PA USA, June , 2008. PDF | PS| Bibtex | Abstract

Intruder deduction problem constitutes the first step in cryptographic protocols verification for a passive intruder. In the case of an active intruder, we know that undecidability of the unification problem implies undecidability of the secrecy problem. In this paper, we analyze the link between the unification problem and the intruder deduction problem. Through examples using equational theories, we show that these two problems are not linked. We present situations where one problem is decidable and the other one is not, or the both are decidable or not. All these examples prove that the two problems are independent for a passive intruder.

@inproceedings{Laf-secret08,
address = {Pittsburg, PA USA},
author = {Lafourcade, Pascal},
booktitle = {{P}roceedings of the 3rd {I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques ({SecReT}'08)},
editor = {},
month = june,
number = {},
pages = {},
publisher = {},
series = {},
title = {Relation between Unification Problem and Intruder Deduction Problem},
volume = {},
year = {2008},
}

[CDELL08b] Judicael Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade. and Yassine Lakhnech Automated Proofs for Asymmetric Encryption. In Proceedings of the Workshop on Formal and Computational Cryptography, (FCC'08), June 2008, Pittsburgh PA, USA. PDF | PS | Bibtex

@inproceedings{CDELL-FCC08,
author = {Judicael Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade. and Yassine Lakhnech},
booktitle = {Workshop on Formal and Computational Cryptography, (FCC'08)},
address = {Pittsburgh PA, USA},
editor = {Bruno Blanchet},
month = jun,
pages = {},
title = {Automated Proofs for Asymmetric Encryption},
year = {2008},
}

[CDELL08c] Judicael Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade. and Yassine Lakhnech Automated Proofs for Asymmetric Encryption. In Proceedings of the Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, (FCS-ARSPA-WITS'08), June 2008, Pittsburgh PA, USA. PDF | PS | Bibtex

@inproceedings{CDELL-FCS08,
address = {Pittsburgh PA, USA},
author = {Judicael Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade. and Yassine Lakhnech},
booktitle = {{P}roceedings f the Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, (FCS-ARSPA-WITS'08)},
editor = {Lujo Bauer, Sandro Etal le, Jerry den Hartog, Luca Vigan\`o},
month = jun,
pages = {109-124},
title = {Automated Proofs for Asymmetric Encryption},
year = {2008},
}

[CL07] Cas Cremers and Pascal Lafourcade. Comparing State Spaces in Automatic Security Protocol Verification. In Michael Goldsmith and Bill Roscoe (eds.), Proceedings of the 7th International Workshop on Automated Verification of Critical Systems (AVoCS'07), Oxford, UK, September 2007, Electronic Notes in Theoretical Computer Science, pages 49-63. Elsevier Science Publishers. PDF | Bibtex | Abstract

Many tools exist for automatic security protocol verification, and most of them have their own particular language for specifying protocols and properties. Several protocol specification models and security properties have been already formally related to each other. However, there is a further difference between verification tools, which has not been investigated in depth before: the explored state space. Some tools explore all possible behaviors, whereas others explore strict subsets, often by using so-called scenarios. Ignoring such differences can lead to wrong interpretations of the output of a tool. We relate the explored state spaces to each other and find previously unreported differences between the various approaches. We apply our study of state space relations in a performance comparison of several well-known automatic tools for security protocol verification. We model a set of protocols and their properties as homogeneous as possible for each tool. We analyze the performance of the tools over comparable state spaces. This work allows us for the first time to compare these automatic tools fairly, i.e., using the same protocol description and exploring the same state space. We also propose some explanations for our experimental results, leading to a better understanding of the tools.

@inproceedings{CL-avocs07,
address = {Oxford, UK},
author = {Cremers, Cas and Lafourcade, Pascal},
booktitle = {{P}roceedings of the 7th {I}nternational {W}orkshop on {A}utomated {V}erification of {C}ritical {S}ystems ({AVoCS}'07)},
editor = {Goldsmith, Michael and Roscoe, Bill},
month = sep,
pages = {49-63},
publisher = {Elsevier Science Publishers},
series = {Electronic Notes in Theoretical Computer Science},
title = {Comparing State Spaces in Automatic Security Protocol Verification},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CL-avocs07.pdf},
year = {2007},
}

[KL07] Bogdan Ksiezopolski and Pascal Lafourcade. Attack and Revison of an Electronic Auction Protocol using OFMC. Technical Report 549, Department of Computer Science, ETH Zurich, Switzerland, February 2007. 13 pages. PDF | Bibtex | Abstract

In the article we show an attack on the cryptographic protocol of electronic auction with extended requirements [Ksiezopolski and Kotulski, Cryptographic protocol for electronic auctions with extended requirements, 2004]. The found attack consists of authentication breach and secret retrieval. It is a kind of man-in-the-middle attack. The intruder impersonates an agent and learns some secret information. We have discovered this flaw unsing OFMC an automatic tool of cryptographic protocol verification. After a description of this attack, we propose a new version of the e-auction protocol. We also check with OFMC the secrecy for the new protocol and give an informal proof of the other properties that this new e-auction protocol has to guarantee.

@techreport{KL-eth07,
author = {Ksi{\k e}{\. z}opolski, Bogdan and Lafourcade, Pascal},
institution = {Department of Computer Science, ETH Zurich, Switzerland},
month = feb,BR> note = {13~pages},
number = {549},
type = {Technical Report},
title = {Attack and Revison of an Electronic Auction Protocol using~{OFMC}},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KL-eth549.pdf},
year = {2007},
}

[LLT06] Pascal Lafourcade, Denis Lugiez and Ralf Treinen. ACUNh: Unification and Disunification Using Automata Theory. In Jordi Levy (ed.), Proceedings of the 20th International Workshop on Unification (UNIF'06), Seattle, Washington, USA, August 2006, pages 6-20. PDF | PS| PS.GZ | Bibtex | Abstract

We show several results about unification problems in the equational theory ACUNh consisting of the theory of exclusive or with one homomorphism. These results are shown using only techniques of automata and combinations of unification problems. We show how to construct a most-general unifier for ACUNh-unification problems with constants using automata. We also prove that the first-order theory of ground terms modulo ACUNh is decidable if the signature does not contain free non-constant function symbols, and that the existential fragment is decidable in the general case. Furthermore, we show a technical result about the set of most-general unifiers obtained for general unification problems.

@inproceedings{LLT-unif2006,
address = {Seattle, Washington, USA},
author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
booktitle = {{P}roceedings of the 20th {I}nternational {W}orkshop on {U}nification ({UNIF}'06)},
editor = {Levy, Jordi},
month = aug,
pages = {6-20},
title = {{ACUNh}: Unification and Disunification Using Automata Theory},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LLT-unif06.pdf},
year = {2006},
}

[LLT05b] Pascal Lafourcade, Denis Lugiez and Ralf Treinen. Intruder Deduction for the Equational Theory of Exclusive-or with Distributive Encryption. Research Report LSV-05-19, Laboratoire Spécification et Vérification, ENS Cachan, France, October 2005. 39 pages. PDF | PS| PS.GZ | Bibtex | Abstract

Cryptographic protocols are small programs which involve a high level of concurrency and which are difficult to analyze by hand. The most successful methods to verify such protocols are based on rewriting techniques and automated deduction in order to implement or mimic the process calculus describing the execution of a protocol.
We are interested in the intruder deduction problem, that is the vulnerability to passive attacks, in presence of the theory of an encryption operator which distributes over the exclusive-or. This equational theory describes very common properties of cryptographic primitives. Solutions to the intruder deduction problem modulo an equational theory are known for the cases of exclusive-or, of Abelian groups, of a homomorphism symbol alone, and of combinations of these theories. In this paper we consider the case where the encryption distributes over exclusive-or. The interaction of the distributive law of the encryption with the cancellation law of exclusive-or leads to a much more complex decision problem. We prove decidability of the intruder deduction problem for an encryption which distributes over exclusive-or with an EXPTIME procedure and we give a PTIME decision procedure relying on prefix rewrite systems for a restricted case, the binary case.

@techreport{LSV:05:19,
author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France},
month = oct,
note = {39~pages},
number = {LSV-05-19},
type = {Research Report},
title = {Intruder Deduction for the Equational Theory of Exclusive-or with Distributive Encryption},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/ rr-lsv-2005-19.pdf},
year = {2005},
}

[Laf03] Pascal Lafourcade. Application de la résolution de conflits 'logiques', à l'aide à la décision pour la résolution de aux conflits des problèmes d'ordonnancement. Rapport de DEA, DEA Représentation de la Connaissance et Fomalisation du Raisonnement, Toulouse, France, June 2003. 66 pages. PS| PS.GZ | Bibtex | Abstract

Lorsqu'il n'existe pas de solution à un problème d'ordonnancement, le calcul des conflits, ensembles minimaux de contraintes « incohérents », donne les explications de cet échec. Cette notion de conflits existe aussi en logique propositionnelle (ensembles minimaux de formules inconsistantes). Nous allons adapter de nombreux critères de préférences locales issus de la résolution de conflits en logique propositionnelle, à la résolution de conflits dans un problème d'ordonnancement. Nous introduisons également de nouveaux critères « colorés » spécifiques aux problèmes d'ordonnancement. Ce cadre formel d'aide à la décision permet de transformer un problème d'ordonnancement sans solution en un problème d'ordonnancement avec solution, en respectant les préférences locales. Nous spécifions pour tous nos critères des algorithmes de type « Branch-and-Bound » pour la recherche de solutions optimales. L'implémentation de certains critères nous montre que l'ordre de résolution des conflits est crucial et confirme que la résolution de tels conflits est un problème exponentiel.

@mastersthesis{Lafourcade-DEA,
author = {Lafourcade, Pascal},
month = jun,
note = {66~pages},
school = {{DEA} Repr{\'e}sentation de la Connaissance et Fomalisation du Raisonnement, Toulouse, France},
type = {Rapport de {DEA}},
title = {Application de la r{\'e}solution de conflits <<~logiques~>>, {\`a} l'aide {\`a} la d{\'e}cision pour la r{\'e}solution de aux conflits des probl{\`e}mes d'ordonnancement},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/lafourca-dea03.ps},
year = {2003},
}

Contract Reports

[BCC+04] Vincent Bernat, Hubert Comon-Lundh, Véronique Cortier, Stéphanie Delaune, Florent Jacquemard, Pascal Lafourcade, Yassine Lakhnech and Laurent Mazaré. Sufficient conditions on properties for an automated verification: theoretical report on the verification of protocols for an extended model of the intruder. Technical Report 4, projet RNTL PROUVé, December 2004. 33 pages. PS| PS.GZ | Bibtex | Abstract

Cryptographic protocols are successfully analyzed using formal methods. However, formal approaches usually consider the encryption schemes as black boxes and assume that an adversary cannot learn anything from an encrypted message except if he has the key. Such an assumption is too strong in general since some attacks exploit in a clever way the interaction between protocol rules and properties of cryptographic operators. Moreover, the executability of some protocols relies explicitly on some algebraic properties of cryptographic primitives such as commutative encryption. We first give an overview of the existing methods in formal approaches for analyzing cryptographic protocols. Then we describe more precisely the results obtained by the partners of the RNTL project PROUVÉ.

@techreport{Prouve:rap4,
author = {Bernat, Vincent and Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique and Delaune, St{\'e}phanie and Jacquemard, Florent and Lafourcade, Pascal and Lakhnech, Yassine and Mazar{\'e}, Laurent},
institution = {projet RNTL PROUV{\'E}},
month = dec,
note = {33~pages},
number = {4},
type = {Technical Report},
title = {Sufficient conditions on properties for an automated verification: theoretical report on the verification of protocols for an extended model of the intruder},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/prouve-rap4.ps},
year = {2004},
}