Conferences
[DGKLL15] Jannik Dreier, Rosario Giustolisi, Ali Kassem, Pascal
Lafourcade, and Gabriele Lenzini: A Framework for Analyzing
Verifiability in Traditional and Electronic Exams. ISPEC 2015, pages
514529
[KFL15] Ali Kassem, Yliès Falcone, and Pascal Lafourcade :
Monitoring Electronic Exams. The 15th International Conference on
Runtime Verification, September, 2015 Vienna,
Austria
[DKL'15] Jannik Dreier, Ali Kassem, and Pascal Lafourcade: Formal
Analysis of ECash Protocols. In 11th International Joint Conference
on eBusiness and Telecommunications (SECRYPT 2015).
[AGLM'15] Affoua Théràse Aby, Alexandre Guitton,
Pascal Lafourcade, and Michel Misson. SLACK_MAC: Adaptive MAC
Protocol for Low DutyCycle Wireless Sensor Networks. ADHOCNETS 2015.
[DGK+14] Jannik Dreier, Rosario Giustolisi, Ali Kassem, Pascal
Lafourcade, Gabriele Lenzin,and Peter
Y.A. Ryan. Formal analysis of
electronic exams. In 11th International Joint Conference on
eBusiness and Telecommunications (SECRYPT 2014),
2014. Best
Paper
Award. PDF
[DJL14] Jannik Dreier, Hugo Jonker, and Pascal
Lafourcade. Secure auctions without
cryptography. In Alfredo Ferro, Fabrizio Luccio, and Peter Widmayer,
editors, Fun with Algorithms  7th International Conference, FUN
2014, Lipari Island, Sicily, Italy, July 13, 2014. Proceedings,
volume 8496 of Lecture Notes in Computer Science, pages
158170. Springer, 2014. PDF
[JL14b] Raphël Jamet and Pascal Lafourcade. (In)corruptibility of routing
protocols. In Foundations and Practice of Security  7th
International Symposium, FPS 2014, Montréal, Canada, 2014, Lecture
Notes in Computer Science. Springer, 2014. Best Paper Award. PDF
[KLL14a] Ali Kassem, Pascal Lafourcade, and Yassine
Lakhnech. Formal verification
of ereputation protocols. In Foundations and Practice of Security
 7th International Symposium, FPS 2014, Montréal, Canada,
Lecture Notes in Computer Science. Springer,
2014. PDF
[KLL14c] Amrit Kumar, Pascal Lafourcade, and Cédric
Lauradoux. Performances of
cryptographic accumulators. In The 39th IEEE Conference on Local
Computer Networks (LCN), 2014. PDF
[MCL+14a]
Ismail Mansour, Gérard Chalhoub, Pascal Lafourcade, and Francois
Delobel. Secure key renewal and revocation for wireless sensor
networks. In The 39th IEEE Conference on Local Computer Networks
(LCN), Edmonton, Canada, 2014. PDF
[MRC+14] Ismail Mansour, Damian Rusinek, Gérard Chalhoub,
Pascal Lafourcade, and Bogdan
Ksiezopolski. Multihop node authentication
mechanisms for wireless sensor networks. In Song Guo, Jaime
Lloret, Pietro Manzoni, and Stefan Ruehrup, editors, Adhoc, Mo
bile, and Wireless Networks  13th International Conference,
ADHOCNOW 2014, Benidorm, Spain, June 2227, 2014 Proceedings,
volume 8487 of Lecture Notes in Computer Science, pages 402 
418. Springer, 2014. PDF
[DLL13] Jannik Dreier, Pascal Lafourcade, Yassine Lakhnech:
Formal verification of eauction protocols.
In David A. Basin and John C. Mitchell, editors, POST, volume 7796 of Lecture Notes in Computer Science, pages 247266. Springer, 2013.
PDF

Bibtex 
Abstract
@inproceedings{DLL13,
author = {Jannik Dreier and
Pascal Lafourcade and
Yassine Lakhnech},
title = {Formal Verification of eAuction Protocols},
pages = {247266},
editor = {David A. Basin and
John C. Mitchell},
booktitle = {Principles of Security and Trust  Second International
Conference, POST 2013, Held as Part of the European Joint
Conferences on Theory and Practice of Software, ETAPS 2013,
Rome, Italy, March 1624, 2013. Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7796},
year = {2013},
}
Auctions have a long history, having been recorded as early as 500
B.C.. With the rise of Internet, electronic auctions have been a great
success and are increasingly used. Many cryptographic protocols have
been proposed to address the various security requirements of these
electronic transactions. We propose a formal framework to analyze and
verify security properties of eAuction protocols. We model protocols
in the Applied $\pi$Calculus and define privacy notions, which
include secrecy of bids, anonymity of the participants,
receiptfreeness and coercionresistance. We also discuss fairness,
nonrepudiation and noncancellation. Additionally we show on two case
studies how these properties can be verified automatically using
ProVerif, and discover several attacks.
[DJL13] Jannik Dreier, Hugo Jonker, and Pascal
Lafourcade.
Verifiability in eauction protocols.
In 8th ACM Symposium on Information, Computer and Communications Security,
ASIACCS 2013, Hangzhou, China, 2013. to appear.
PDF

Bibtex 
Abstract
@inproceedings{DJL13,
author = {Jannik Dreier and Hugo Jonker and Pascal Lafourcade},
title ={Verifiability in eAuction Protocols},
booktitle = {8th ACM Symposium on Information, Computer and Communications Security, ASIACCS 2013},
address={Hangzhou, China},
year = {2013},
note ={to appear},
}
An electronic auction
protocol will only be used by those who trust that it operates
correctly. Therefore, eauct ion protocols must be verifiable :
seller, buyer and losing bidders must all be able to determine that
the result was correct. We pose that the importance of verifiability
for eauctions neces sitates a formal analysis. Consequently, we
identify notions of verifiability for each stakeholder. We formalize
these and then use the developed framework to study the verifiability
of two examples. We provide an analysis We identify issues with the
protocol due to Curtis et al. and the one by Brandt.
[ADJL13] Karine Altisen, St&ecute;phane Devismes, Raphael Jamet, and
Pascal Lafourcade.
SR3: Secure resilient reputationbased routing.
In The annual IEEE International Conference on Distributed Computing in
Sensor Systems (DCOSS 2013), Cambridge, Massachusetts, USA, may
2013. to appear.
PDF

Bibtex 
Abstract
@inproceedings{ADJL13,
author = {Karine Altisen and St\'ephane Devismes and Rapha"el Jamet and Pascal Lafourcade},
title = {{SR3}: Secure Resilient Reputationbased Routing},
booktitle = {The annual IEEE International Conference on Distributed Computing in Sensor Systems (DCOSS 2013)},
year={2013},
note={to appear},
address={Cambridge, Massachusetts, USA},
month = {may},
}
We propose SR3, a secure and resilient algorithm for convergecast
routing in WSNs. SR3 uses lightweight cryptographic primitives to
achieve data confidentiality and data packet unforgeability. SR3
has a security proven by formal tool. We made simulations to show
the resiliency of SR3 against various scenarios, where we mixed
selective forwarding, blackhole, wormhole, and Sybil attacks. We
compared our solution to several routing algorithms of the
literature. Our results show that the resiliency accomplished by
SR3 is drastically better than the one achieved by those protocols,
especially when the network is sparse. Moreover, unlike previous
solutions, SR3 selfadapts after compromised nodes suddenly change
their behavior.
[DELL13] Jannik Dreier, Cristian Ene, Pascal Lafourcade, and Yassine
Lakhnech.
On unique decomposition of processes in the appliedcalculus.
In Frank Pfenning, editor, FoSSaCS, volume 7794 of Lecture
Notes in Computer Science, pages 5064. Springer, 2013.
PDF

Bibtex 
Abstract
@inproceedings{DELL13,
author = {Jannik Dreier and
Cristian Ene and
Pascal Lafourcade and
Yassine Lakhnech},
title = {On Unique Decomposition of Processes in the Applied Calculus},
pages = {5064},
editor = {Frank Pfenning},
booktitle = {Foundations of Software Science and Computation Structures
 16th International Conference, FOSSACS 2013, Held as Part
of the European Joint Conferences on Theory and Practice
of Software, ETAPS 2013, Rome, Italy, March 1624, 2013.
Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7794},
year = {2013},
}
Unique decomposition has been a subject of interest in process algebra
for a long time (for example in BPP [Christensen93] or CCS
[Milner93,Moller89]), as it provides a normal form with useful
cancellation properties. We provide two parallel decomposition
results for subsets of the picalculus: we show that any closed
normed (i.e. with a finite shortest complete trace) process P can
be decomposed uniquely into prime factors $ with respect to
strong labeled bisi milarity, i.e. such that \sim_l P_1  \ldots 
P_n$. We also prove that close d finite processes can be decomposed
uniquely with respect to weak labeled bisimilarity.
[DDL13] Jannik Dreier, JeanGuillaume Dumas, and Pascal
Lafourcade.
Brandt's fully private auction protocol revisited.
In 6th
International Conference on Cryptology in Africa Africacrypt 2013,
Egypt, june 2013. to appear.
PDF

Bibtex 
Abstract
@inproceedings{DDL13,
}
Auctions have a long
history, having been recorded as early as 500
B.C. [Krishna02]. Nowadays, electronic auctions have been a great
success and are increasingly used. Many cryptographic protocols have
been proposed to address the various security requirements of these
electronic transactions, in particular to ensure privacy. [Brandt06]
developed a protocol that computes the winner using homomorphic
operations on a distributed ElGamal encryption of the bids. He claimed
that it ensures full privacy of the bidders, i.e. no information apart
from the winner and the winning price is leaked. We first show that
this protocol  when using malleable interactive zeroknowledge
proofs  is vulnerable to attacks by dishonest bidders. Such bidders
can manipulate the publicly available data in a way that allows the
seller to deduce all participants' bids. Additionally we discuss some
issues with verifiability as well as attacks on nonrepudiation,
fairness and the privacy of individual bidders exploiting
authentication problems.
[DLL12] Jannik Dreier, Pascal Lafourcade, Yassine Lakhnech:
Defining Privacy for Weighted Votes, Single and MultiVoter Coercion. . European Symposium on Research in Computer Security (ESORICS), 2012.
PDF

Bibtex 
Abstract 
Technical Report
@inproceedings{DLL12,
title = {Defining Privacy for Weighted Votes, Single and MultiVoter Coercion},
author = {Jannik Dreier and Pascal Lafourcade and Yassine Lakhnech},
year = {2012},
booktitle = {ESORICS 2012},
pages = {},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {},
team = {DCS},
}
Most existing formal privacy definitions for voting protocols are
based on observational equivalence between two situations where two
voters swap their votes. These definitions are unsuitable for cases
where votes are weighted. In such a case swapping two votes can result
in a different outcome and both situations become trivially
distinguishable. We present a definition for privacy in voting
protocols in the Applied piCalculus that addresses this
problem. Using our model, we are also able to define multivoter
coercion, i.e. situations where several voters are attacked at the
same time. Then we prove that under certain realistic assumptions a
protocol secure against coercion of a single voter is also secure
against coercion of multiple voters. This applies for Receipt
Freeness as well as CoercionResistance.
[AGDL12]
Karine Altisen, Stéphane Devismes, Antoine Gerbaud, Pascal Lafourcade:
Analysis of Random Walks Using Tabu Lists.. In Structural Information and Communication Complexity  19th
International Colloquium, SIROCCO 2012, Reykjavik, Iceland,
June 30July 2,2012.
PDF

Bibtex 
Abstract
@inproceedings{AGDL12,
title = {Analysis of Random Walks Using Tabu Lists},
author = {Karine Altisen and
St{\'e}phane Devismes and
Antoine Gerbaud and
Pascal Lafourcade},
year = {2012},
booktitle = {Structural Information and Communication Complexity  19th
International Colloquium, SIROCCO 2012. Proceedings},
pages = {254266},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7355},
team = {DCS},
}
A tabu random walk on a graph is a partially selfavoiding random walk
which uses a bounded memory to avoid cycles. This memory is called a
tabu list and contains vertices already visited by the walker. The
size of the tabu list being bounded, the way vertices are inserted and
removed from the list, called here an update rule, has an important
impact on the performance of the walk, namely the mean hitting time
between two given vertices. We define a large class of tabu random
walks, characterized by their update rules. We enunciate a necessary
and sufficient condition on these update rules that ensures the
finiteness of the mean hitting time of their associated walk on every
finite and connected graph. According to the memory allocated to the
tabu list, we characterize the update rules which yield smallest mean
hitting times on a large class of graphs. Finally, we compare the
performances of three collections of classical update rules according
to the size of their associated tabu list.
[DLL12b] Jannik Dreier, Pascal Lafourcade, Yassine Lakhnech.
A Formal Taxonomy of Privacy in Voting
Protocols. First IEEE International Workshop on Security and
Forensics in Communication Systems (ICC'12 WS  SFCS), 2012. 

Bibtex 
Abstract 
Technical Report
@inproceedings{DreierSFCS12,
title = {A Formal Taxonomy of Privacy in Voting Protocols},
author = {Jannik Dreier and Pascal Lafourcade and Yassine Lakhnech},
year = {2011},
booktitle = {First IEEE International Workshop on Security and Forensics in Communication Systems (ICC'12 WS  SFCS)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
team = {DCS},
}
Privacy is one of the main issues in electronic voting. We propose a
modular family of symbolic privacy notions that allows to assess the
level of privacy ensured by a voting protocol. Our definitions are
applicable to protocols featuring multiple votes per voter and special
attack scenarios such as votecopying or forced abstention. Finally we
employ our definitions on several existing voting protocols to show
that our model allows to compare different types of protocols based on
different techniques, and is suitable for automated verification using
existing tools.
[GKL12] Key Management Protocol in WIMAX revisited. Ghoualmi, Nacira and Kahya, Noudjoud and Lafourcade, Pascal (in The Third International Conference on Communications Security and Information Assurance (CSIA 2012), 2012)
[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 57,
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 57, 2011. Proceedings},
pages = {348362},
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 multiparty trust computation, noninteractive
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 evoting 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. VoteIndependence: A Powerful Privacy Notion for Voting
Protocols. 4th CanadaFrance 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 ProofofConcept Implementation for Medical Services
with Electronic Health Records. IIHMSP 2010: 510513
PDF 
Bibtex 
Abstract
@inproceedings{TWE+10,
title = {Privacy by Data Provenance with Digital Watermarking  A ProofofConcept 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 (IIHMSP 2010), Darmstadt, Germany, 1517 October, 2010, Proceedings},
pages = {510513},
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
proofofconcept 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.
[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 SafaviNaini
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{GLLSASIAN09,
author = {Martin Gagné, Pascal Lafourcade, Yassine Lakhnech, and Reihaneh SafaviNaini},
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
Chosenciphertext 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 BellareRogaway 1993, REACT and Pointcheval at
PKC'2000.
@inproceedings{CDELLCCS08,
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 = {371380},
publisher = {ACM},
year = {2008},
address = {Alexandria, USA},
}
[Laf07] Pascal Lafourcade.
Intruder Deduction for the
Equational Theory of Exclusiveor 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 3757. 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
socalled passive attacker. We extend the DolevYao model in order to
model this problem in presence of the equational theory of a
commutative encryption operator which distributes over the
exclusiveor operator. The interaction between the commutative
distributive law of the encryption and exclusiveor offers more
possibilities to decrypt an encrypted message than in the
noncommutative 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 exclusiveor with a
DOUBLEEXPTIME procedure. And we obtain that this problem is
EXPSPACEhard in the binary case.
@inproceedings{Lafsecret06,
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 = {3757},
publisher = {Elsevier Science Publishers},
series = {Electronic Notes in Theoretical Computer Science},
title = {Intruder Deduction for the Equational Theory of {mph{Exclusiveor}} with Commutative and Distributive Encryption},
url = {http://www.lsv.enscachan.fr/Publis/PAPERS/PDF/Lafsecret06long.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
132143. 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 welldefined 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{DLLTICALP2006,
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 = {132143},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Symbolic Protocol Analysis in Presence of a Homomorphism Operator and {mph{Exclusive~Or}}},
url = {http://www.lsv.enscachan.fr/Publis/PAPERS/PDF/DLLTicalp06.pdf},
volume = {4052},
year = {2006},
}
[LLT05a] Pascal Lafourcade, Denis Lugiez and Ralf Treinen.
Intruder Deduction for AClike
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 308322. 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 AClike
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 AClike
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 onecounter and pushdown automata.
@inproceedings{LLTrta2005,
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 = {308322},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Intruder Deduction for {AC}like Equational Theories with Homomorphisms},
url = {http://www.lsv.enscachan.fr/Publis/PAPERS/PDF/rta05LLT.pdf},
volume = {3467},
year = {2005},
}