Selected publications by Stéphanie Delaune

Chapters in Books

CDM11

H. Comon-Lundh, S. Delaune and J. Millen.  Constraint solving techniques and enriching the model with equational theories.  In Formal Models and Techniques for Analyzing Security Protocols, Cryptology and Information Security Series 5, pages 35-61. IOS Press, 2011. ( PDF | BibTeX + Abstract )

DKR10a

S. Delaune, S. Kremer and M. D. Ryan.  Verifying Privacy-Type Properties of Electronic Voting Protocols: A Taster.  In Towards Trustworthy Elections - New Directions in Electronic Voting, LNCS 6000, pages 289-309. Springer, 2010. ( PDF | BibTeX + Abstract )

Journals

BCD13

S. Bursuc, H. Comon-Lundh and S. Delaune.  Deducibility constraints and blind signatures.  Information and Computation, 2013. To appear. ( PDF | BibTeX + Abstract )

CDKR13

C. Chevalier, S. Delaune, S. Kremer and M. Ryan.  Composition of Password-based Protocols.  Formal Methods in System Design, 2013. To appear. ( PDF | BibTeX + Abstract )

BCD12

M. Baudet, V. Cortier and S. Delaune.  YAPA: A generic tool for computing intruder knowledge.  ACM Transactions on Computational Logic, 2012. To appear. ( PDF | BibTeX + Abstract )

CD12

V. Cortier and S. Delaune.  Decidability and combination results for two notions of knowledge in security protocols.  Journal of Automated Reasoning 48(4), pages 441-487, 2012. ( PDF | BibTeX + Abstract )

CDK12

Ş. Ciobâcă, S. Delaune and S. Kremer.  Computing knowledge in security protocols under convergent equational theories.  Journal of Automated Reasoning 48(2), pages 219-262, 2012. ( PDF | BibTeX + Abstract )

DKS10

S. Delaune, S. Kremer and G. Steel.  Formal Analysis of PKCS#11 and Proprietary Extensions.  Journal of Computer Security 18(6), pages 1211-1245, 2010. ( PDF | BibTeX + Abstract )

DKR10b

S. Delaune, S. Kremer and M. D. Ryan.  Symbolic bisimulation for the applied pi calculus.  Journal of Computer Security 18(2), pages 317-377, 2010. ( PDF | BibTeX + Abstract )

DKR09

S. Delaune, S. Kremer and M. D. Ryan.  Verifying Privacy-type Properties of Electronic Voting Protocols.  Journal of Computer Security 17(4), pages 435-487, 2009. ( PDF | PS | PS.GZ | BibTeX + Abstract )

CD09a

V. Cortier and S. Delaune.  Safely Composing Security Protocols.  Formal Methods in System Design 34(1), pages 1-36, 2009. ( PDF | PS | PS.GZ | BibTeX + Abstract )

DLLT08

S. Delaune, P. Lafourcade, D. Lugiez and R. Treinen.  Symbolic protocol analysis for monoidal equational theories.  Information and Computation 206(2-4), pages 312-351, 2008. ( PDF | BibTeX + Abstract )

CDL06

V. Cortier, S. Delaune and P. 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 )

Del06a

S. Delaune.  An Undecidability Result for AGh.  Theoretical Computer Science 368(1-2), pages 161-167, 2006. ( PDF | PS | PS.GZ | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract )

Del06b

S. Delaune.  Easy Intruder Deduction Problems with Homomorphisms.  Information Processing Letters 97(6), pages 213-218, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )

DJ06

S. Delaune and F. Jacquemard.  Decision Procedures for the Security of Protocols with Probabilistic Encryption against Offline Dictionary Attacks.  Journal of Automated Reasoning 36(1-2), pages 85-124, 2006. ( PS | PS.GZ | BibTeX + Abstract )

Conferences

CCD13

R. Chrétien, V. Cortier and S. Delaune.  From security protocols to pushdown automata.  In ICALP'13, LNCS. Springer, 2013. To appear. ( PDF | PDF (long version) | BibTeX + Abstract )

CD13

R. Chrétien and S. Delaune.  Formal analysis of privacy for routing protocols in mobile ad hoc networks.  In POST'13, LNCS. Springer, 2013. To appear. ( PDF | PDF (long version) | BibTeX + Abstract )

ACD12

M. Arapinis, V. Cheval and S. Delaune.  Verifying privacy-type properties in a modular way.  In CSF'12, pages 95-109. IEEE Computer Society Press, 2012. ( PDF | PDF (long version) | BibTeX + Abstract )

DKP12

S. Delaune, S. Kremer and D. Pasailă.  Security protocols, constraint systems, and group theories.  In IJCAR'12, LNAI 7364, pages 164-178. Springer-Verlag, 2012. ( PDF | PDF (long version) | BibTeX + Abstract )

CDD12

V. Cortier, J. Degrieck and S. Delaune.  Analysing routing protocols: four nodes topologies are sufficient.  In POST'12, LNCS 7215, pages 30-50. Springer, 2012. ( PDF | PDF (long version) | BibTeX + Abstract )

DDS12

M. Dahl, S. Delaune and G. Steel.  Formal Analysis of Privacy for Anonymous Location Based Services.  In TOSCA'11, LNCS 6993, pages 98-112. Springer, 2012. ( PDF | BibTeX + Abstract )

CDK11

C. Chevalier, S. Delaune and S. Kremer.  Transforming Password Protocols to Compose.  In FSTTCS'11, Leibniz International Proceedings in Informatics 13, pages 204-216. Leibniz-Zentrum für Informatik, 2011. ( PDF | PDF (long version) | BibTeX + Abstract )

CCD11

V. Cheval, H. Comon-Lundh and S. Delaune.  Trace Equivalence Decision: Negative Tests and Non-determinism.  In CCS'11, pages 321-330. ACM Press, 2011. ( PDF | BibTeX + Abstract )

ACD11a

M. Arnaud, V. Cortier and S. Delaune.  Deciding security for protocols with recursive tests.  In CADE'11, LNAI, pages 49-63. Springer, 2011. ( PDF | PDF (long version) | BibTeX + Abstract )

DKRS11

S. Delaune, S. Kremer, M. D. Ryan and G. Steel.  Formal analysis of protocols based on TPM state registers.  In CSF'11, pages 66-82. IEEE Computer Society Press, 2011. ( PDF | BibTeX + Abstract )

DDS10a

M. Dahl, S. Delaune and G. Steel.  Formal Analysis of Privacy for Vehicular Mix-Zones.  In ESORICS'10, LNCS 6345, pages 55-70. Springer, 2010. ( PDF | PS | PS.GZ | BibTeX + Abstract )

DKRS10a

S. Delaune, S. Kremer, M. D. Ryan and G. Steel.  A Formal Analysis of Authentication in the TPM.  In FAST'10, LNCS 6561, pages 111-125. Springer, 2010. ( PDF | PS | PS.GZ | BibTeX + Abstract )

ACD10

M. Arnaud, V. Cortier and S. Delaune.  Modeling and Verifying Ad Hoc Routing Protocols.  In CSF'10, pages 59-74. IEEE Computer Society Press, 2010. ( PDF | PDF (long version) | BibTeX + Abstract )

CCD10

V. Cheval, H. Comon-Lundh and S. Delaune.  Automating security analysis: symbolic equivalence of constraint systems.  In IJCAR'10, LNAI 6173, pages 412-426. Springer-Verlag, 2010. ( PDF | BibTeX + Abstract )

BDC09

S. Bursuc, S. Delaune and H. Comon-Lundh.  Deducibility constraints.  In ASIAN'09, LNCS 5913, pages 24-38. Springer, 2009. ( PDF | PS | PS.GZ | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract )

DKP09

S. Delaune, S. Kremer and O. Pereira.  Simulation based security in the applied pi calculus.  In FSTTCS'09, Leibniz International Proceedings in Informatics 4, pages 169-180. Leibniz-Zentrum für Informatik, 2009. ( PDF | PDF (long version) | BibTeX + Abstract )

CDK09a

Ş. Ciobâcă, S. Delaune and S. Kremer.  Computing knowledge in security protocols under convergent equational theories.  In CADE'09, LNAI, pages 355-370. Springer, 2009. ( PDF | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract )

CD09b

V. Cortier and S. Delaune.  A method for proving observational equivalence.  In CSF'09, pages 266-276. IEEE Computer Society Press, 2009. ( PDF | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract )

BCD09

M. Baudet, V. Cortier and S. Delaune.  YAPA: A generic tool for computing intruder knowledge.  In RTA'09, LNCS 5595, pages 148-163. Springer, 2009. ( PDF | PDF (long version) | PS (long version) | PS.GZ (long version) | Slides | BibTeX + Abstract )

CDK09b

R. Chadha, S. Delaune and S. Kremer.  Epistemic Logic for the Applied Pi Calculus.  In FMOODS/FORTE'09, LNCS 5522, pages 182-197. Springer, 2009. ( PDF | PS | PS.GZ | BibTeX + Abstract )

ADK08

M. Arapinis, S. Delaune and S. Kremer.  From One Session to Many: Dynamic Tags for Security Protocols.  In LPAR'08, LNAI 5330, pages 128-142. Springer, 2008. ( PDF | PDF (long version) | BibTeX + Abstract )

DKR08

S. Delaune, S. Kremer and M. D. Ryan.  Composition of Password-based Protocols.  In CSF'08, pages 239-251. IEEE Computer Society Press, 2008. ( PDF | BibTeX + Abstract )

DKS08

S. Delaune, S. Kremer and G. Steel.  Formal Analysis of PKCS#11.  In CSF'08, pages 331-344. IEEE Computer Society Press, 2008. ( PDF | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract )

DRS08

S. Delaune, M. D. Ryan and B. Smyth.  Automatic verification of privacy properties in the applied pi-calculus.  In IFIPTM'08, IFIP Conference Proceedings 263, pages 263-278. Springer, 2008. ( PDF | PS | PS.GZ | PDF (long version) | BibTeX + Abstract )

CDD07

V. Cortier, J. Delaitre and S. Delaune.  Safely Composing Security Protocols.  In FSTTCS'07, LNCS 4855, pages 352-363. Springer, 2007. ( PDF | PDF (long version) | BibTeX + Abstract )

DKR07a

S. Delaune, S. Kremer and M. D. Ryan.  Symbolic Bisimulation for the Applied Pi-Calculus.  In FSTTCS'07, LNCS 4855, pages 133-145. Springer, 2007. ( PDF | PDF (long version) | BibTeX + Abstract )

CD07a

V. Cortier and S. Delaune.  Deciding Knowledge in Security Protocols for Monoidal Equational Theories.  In LPAR'07, LNAI 4790, pages 196-210. Springer, 2007. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )

DLL07a

S. Delaune, H. Lin and Ch. Lynch.  Protocol verification via rigid/flexible resolution.  In LPAR'07, LNAI 4790, pages 242-256. Springer, 2007. ( BibTeX + Abstract )

ACD07

M. Arnaud, V. Cortier and S. Delaune.  Combining algorithms for deciding knowledge in security protocols.  In FroCoS'07, LNAI 4720, pages 103-117. Springer, 2007. ( PDF | PS | PS.GZ | PDF (long version) | Slides | BibTeX + Abstract )

CDS07

V. Cortier, S. Delaune and G. Steel.  A Formal Theory of Key Conjuring.  In CSF'07, pages 79-93. IEEE Computer Society Press, 2007. ( PDF | PS | PS.GZ | PDF (long version) | Slides | BibTeX + Abstract )

BCD07a

S. Bursuc, H. Comon-Lundh and S. Delaune.  Deducibility Constraints, Equational Theory and Electronic Money.  In Rewriting, Computation and Proof, LNCS 4600, pages 196-212. Springer, 2007. ( PS | PS.GZ | BibTeX + Abstract )

BCD07b

S. Bursuc, H. Comon-Lundh and S. Delaune.  Associative-Commutative Deducibility Constraints.  In STACS'07, LNCS 4393, pages 634-645. Springer, 2007. ( PDF | PS | PS.GZ | BibTeX + Abstract )

DKR06a

S. Delaune, S. Kremer and M. D. Ryan.  Coercion-Resistance and Receipt-Freeness in Electronic Voting.  In CSFW'06, pages 28-39. IEEE Computer Society Press, 2006. ( PDF | PS | PS.GZ | PDF (long version) | PS (long version) | PS.GZ (long version) | Slides | BibTeX + Abstract )

DLLT06

S. Delaune, P. Lafourcade, D. Lugiez and R. Treinen.  Symbolic Protocol Analysis in Presence of a Homomorphism Operator and Exclusive Or.  In ICALP'06, LNCS 4052, pages 132-143. Springer, 2006. ( PDF | PS | PS.GZ | PDF (long version) | PS (long version) | PS.GZ (long version) | BibTeX + Abstract )

CD05

H. Comon-Lundh and S. Delaune.  The finite variant property: How to get rid of some algebraic properties.  In RTA'05, LNCS 3467, pages 294-307. Springer, 2005. ( PDF | PS | PS.GZ | PS (long version) | PS.GZ (long version) | Slides | BibTeX + Abstract )

DJ04a

S. Delaune and F. Jacquemard.  A Decision Procedure for the Verification of Security Protocols with Explicit Destructors.  In CCS'04, pages 278-287. ACM Press, 2004. ( PS | PS.GZ | PS (long version) | PS.GZ (long version) | Slides | BibTeX + Abstract )

DJ04b

S. Delaune and F. Jacquemard.  A Theory of Dictionary Attacks and its Complexity.  In CSFW'04, pages 2-15. IEEE Computer Society Press, 2004. ( PS | PS.GZ | PS (long version) | PS.GZ (long version) | Slides | BibTeX + Abstract )

Theses

Del11a

S. Delaune.  Verification of security protocols: from confidentiality to privacy.  Mémoire d'habilitation, École Normale Supérieure de Cachan, France, March 2011. ( PDF | Slides | BibTeX + Abstract )

Del06c

S. Delaune.  Vérification des protocoles cryptographiques et propriétés algébriques.  Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, June 2006. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )

Other Publications

CCD12

V. Cheval, V. Cortier and S. Delaune.  Deciding equivalence-based properties using constraint solving.  Research Report LSV-12-17, Laboratoire Spécification et Vérification, ENS Cachan, France, August 2012. 53 pages. ( PDF | BibTeX + Abstract )

ACD11b

M. Arnaud, V. Cortier and S. Delaune.  Modeling and Verifying Ad Hoc Routing Protocols.  Research Report LSV-11-24, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2011. 66 pages. ( PDF | BibTeX + Abstract )

DKRS10b

S. Delaune, S. Kremer, M. D. Ryan and G. Steel.  A Formal Analysis of Authentication in the TPM (short paper).  In SecCo'10. 2010. ( PDF | PS | PS.GZ | BibTeX )

DDS10b

M. Dahl, S. Delaune and G. Steel.  Formal Analysis of Privacy for Vehicular Mix-Zones.  In FCS-PrivMod'10. 2010. ( PDF | PS | PS.GZ | BibTeX + Abstract )

CCD09

V. Cheval, H. Comon-Lundh and S. Delaune.  A decision procedure for proving observational equivalence.  In SecCo'09. 2009. ( PDF | BibTeX )

ACD09

M. Arnaud, V. Cortier and S. Delaune.  Modeling and Verifying Ad Hoc Routing Protocol.  In SecReT'09, pages 33-46. 2009. ( PDF | PS | PS.GZ | BibTeX + Abstract )

CDK09c

Ş. Ciobâcă, S. Delaune and S. Kremer.  Computing knowledge in security protocols under convergent equational theories.  In SecReT'09, pages 47-58. 2009. ( PDF | BibTeX + Abstract )

DKR07b

S. Delaune, S. Kremer and M. D. Ryan.  Symbolic bisimulation for the applied pi calculus.  In SecCo'07. 2007. Preliminary version of [DKR07a]. ( PDF | PDF (long version) | BibTeX )

CD07b

V. Cortier and S. Delaune.  Deciding knowledge in security protocols for monoidal equational theories.  In FCS-ARSPA'07, pages 63-80. 2007. Preliminary version of [CD07a]. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )

DLL07b

S. Delaune, H. Lin and Ch. Lynch.  Protocol verification via rigid/flexible resolution.  In ADDCT'07, pages 2-16. 2007. Preliminary version of [DLL07a]. ( BibTeX + Abstract )

DKR06b

S. Delaune, S. Kremer and M. D. Ryan.  Verifying Properties of Electronic Voting Protocols.  In WOTE'06, pages 45-52. 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )

DKR05

S. Delaune, S. Kremer and M. D. Ryan.  Receipt-Freeness: Formal Definition and Fault Attacks (Extended Abstract).  In FEE 2005. 2005. Preliminary version of [DKR06a]. ( PDF | BibTeX )

DK04

S. Delaune and F. Klay.  Vérification automatique appliquée à un protocole de commerce électronique.  In JDIR'04, pages 260-269. 2004. ( PDF | Slides | BibTeX + Abstract )

DJ04c

S. Delaune and F. Jacquemard.  Narrowing-Based Constraint Solving for the Verification of Security Protocols.  In UNIF'04. 2004. Preliminary version of [DJ04a]. ( PS | PS.GZ | PS (long version) | PS.GZ (long version) | Slides | BibTeX + Abstract )

Del03a

S. Delaune.  Intruder Deduction Problem in Presence of Guessing Attacks.  In SPV'03, pages 26-30. 2003. ( Slides | BibTeX + Abstract )

Del03b

S. Delaune.  Vérification de protocoles de sécurité dans un modèle de l'intrus étendu.  Rapport de DEA, DEA Programmation, Paris, France, September 2003. ( PS | PS.GZ | Slides | BibTeX )

Del02

S. Delaune.  Utilisation et interface avec une librairie de représentation des contraintes linéaires par des automates.  Research report, Laboratoire d'Informatique Algorithmique, Fondements et Applications, Paris, France, 2002. 16 pages. ( PS | PS.GZ | BibTeX + Abstract )

Contract Reports

Del11b

S. Delaune.  Algorithms for observational equivalence, Deliverable AVOTE 2.2, (ANR-07-SESU-002), 2011. 118 pages. ( PDF | BibTeX )

DK10

S. Delaune and S. Kremer.  Formalising security properties in electronic voting protocols, Deliverable AVOTE 1.2, (ANR-07-SESU-002), 2010. 17 pages. ( PDF | BibTeX + Abstract )

DK09

S. Delaune and S. Kremer.  Spécificités des protocoles de vote électronique, Deliverable AVOTE 1.1 (ANR-07-SESU-002), 2009. 8 pages. ( PDF | BibTeX )

DK07

S. Delaune and F. Klay.  Synthèse des expérimentations.  Technical Report 10, projet RNTL PROUVÉ, May 2007. 10 pages. ( PDF | BibTeX + Abstract )

KBL⁺06

F. Klay, L. Bozga, Y. Lakhnech, L. Mazaré, S. Delaune and S. Kremer.  Retour d'expérience sur la validation du vote électronique.  Technical Report 9, projet RNTL PROUVÉ, November 2006. 47 pages. ( PDF | BibTeX + Abstract )

DKK05

S. Delaune, F. Klay and S. Kremer.  Spécification du protocole de vote électronique.  Technical Report 6, projet RNTL PROUVÉ, November 2005. 19 pages. ( PDF | PS | PS.GZ | BibTeX + Abstract )

BDKV05

L. Bozga, S. Delaune, F. Klay and L. Vigneron.  Retour d'expérience sur la validation du porte-monnaie électronique.  Technical Report 5, projet RNTL PROUVÉ, March 2005. 29 pages. ( PS | PS.GZ | BibTeX + Abstract )

BCC⁺04

V. Bernat, H. Comon-Lundh, V. Cortier, S. Delaune, F. Jacquemard, P. Lafourcade, Y. Lakhnech and L. 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 )

BDKT04

L. Bozga, S. Delaune, F. Klay and R. Treinen.  Spécification du protocole de porte-monnaie électronique.  Technical Report 1, projet RNTL PROUVÉ, June 2004. 12 pages. ( PS | PS.GZ | BibTeX + Abstract )

CDL04

V. Cortier, S. Delaune and P. Lafourcade.  A Survey of Algebraic Properties Used in Cryptographic Protocols.  Technical Report 2, projet RNTL PROUVÉ, June 2004. 19 pages. ( PS | PS.GZ | BibTeX + Abstract )

About LSV

• News
• People
• Research
• Seminars
• Teaching
• Contact

• École Normale Supérieure de Cachan
• Centre National de la Recherche Scientifique