Selected publications by Stéphanie Delaune

Chapters in Books

CD12a
H. Comon-Lundh and S. DelauneFormal Security ProofsIn Software Safety and Security, NATO Science for Peace and Security Series - D: Information and Communication Security 33, pages 26-63. IOS Press, 2012. ( PDF | BibTeX )
CDM11
H. Comon-Lundh, S. Delaune and J. K. MillenConstraint solving techniques and enriching the model with equational theoriesIn 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. RyanVerifying Privacy-Type Properties of Electronic Voting Protocols: A TasterIn Towards Trustworthy Elections - New Directions in Electronic Voting, LNCS 6000, pages 289-309. Springer, 2010. ( PDF | BibTeX + Abstract )

Scientific popularization

CD13a
R. Chrétien and S. DelauneLa protection des informations sensiblesPour La Science 433, pages 70-77, 2013. ( BibTeX )

Journals

ACD14
M. Arnaud, V. Cortier and S. DelauneModeling and Verifying Ad Hoc Routing ProtocolsInformation and Computation, 2014. To appear. ( PDF | BibTeX + Abstract )
BCD14
S. Bursuc, H. Comon-Lundh and S. DelauneDeducibility constraints and blind signaturesInformation and Computation, 2014. To appear. ( PDF | BibTeX + Abstract )
ADK14
M. Arapinis, S. Delaune and S. KremerDynamic Tags for Security ProtocolsLogical Methods in Computer Science 10(2:11), 2014. ( PDF | BibTeX + Abstract )
CDKR13
C. Chevalier, S. Delaune, S. Kremer and M. D. RyanComposition of Password-based ProtocolsFormal Methods in System Design 43(3), pages 369-413, 2013. ( PDF | BibTeX + Abstract )
CCD13a
V. Cheval, V. Cortier and S. DelauneDeciding equivalence-based properties using constraint solvingTheoretical Computer Science 492, pages 1-39, 2013. ( PDF | BibTeX + Abstract )
BCD13
M. Baudet, V. Cortier and S. DelauneYAPA: A generic tool for computing intruder knowledgeACM Transactions on Computational Logic 14(1:4), 2013. ( PDF | BibTeX + Abstract )
CD12b
V. Cortier and S. DelauneDecidability and combination results for two notions of knowledge in security protocolsJournal of Automated Reasoning 48(4), pages 441-487, 2012. ( PDF | BibTeX + Abstract )
CDK12
Ş. Ciobâcă, S. Delaune and S. KremerComputing knowledge in security protocols under convergent equational theoriesJournal of Automated Reasoning 48(2), pages 219-262, 2012. ( PDF | BibTeX + Abstract )
DKS10
S. Delaune, S. Kremer and G. SteelFormal Analysis of PKCS#11 and Proprietary ExtensionsJournal of Computer Security 18(6), pages 1211-1245, 2010. ( PDF | BibTeX + Abstract )
DKR10b
S. Delaune, S. Kremer and M. D. RyanSymbolic bisimulation for the applied pi calculusJournal of Computer Security 18(2), pages 317-377, 2010. ( PDF | BibTeX + Abstract )
DKR09
S. Delaune, S. Kremer and M. D. RyanVerifying Privacy-type Properties of Electronic Voting ProtocolsJournal of Computer Security 17(4), pages 435-487, 2009. ( PDF | PS | PS.GZ | BibTeX + Abstract )
CD09a
V. Cortier and S. DelauneSafely Composing Security ProtocolsFormal 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. TreinenSymbolic protocol analysis for monoidal equational theoriesInformation and Computation 206(2-4), pages 312-351, 2008. ( PDF | BibTeX + Abstract )
CDL06
V. Cortier, S. Delaune and P. LafourcadeA Survey of Algebraic Properties Used in Cryptographic ProtocolsJournal of Computer Security 14(1), pages 1-43, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
Del06a
S. DelauneAn Undecidability Result for AGhTheoretical 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. DelauneEasy Intruder Deduction Problems with HomomorphismsInformation Processing Letters 97(6), pages 213-218, 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
DJ06
S. Delaune and F. JacquemardDecision Procedures for the Security of Protocols with Probabilistic Encryption against Offline Dictionary AttacksJournal of Automated Reasoning 36(1-2), pages 85-124, 2006. ( PS | PS.GZ | BibTeX + Abstract )

Conferences

CCD14
R. Chrétien, V. Cortier and S. DelauneTyping messages for free in security protocols: the case of equivalence propertiesIn CONCUR'14, LNCS 8704. Springer, 2014. To appear. ( BibTeX )
BDH14
D. Baelde, S. Delaune and L. HirschiA reduced semantics for deciding trace equivalence using constraint systemsIn POST'14, LNCS 8414, pages 1-21. Springer, 2014. ( PDF | BibTeX + Abstract )
CCD13b
R. Chrétien, V. Cortier and S. DelauneFrom security protocols to pushdown automataIn ICALP'13, LNCS 7966, pages 137-149. Springer, 2013. ( PDF | PDF (long version) | BibTeX + Abstract )
CD13b
R. Chrétien and S. DelauneFormal analysis of privacy for routing protocols in mobile ad hoc networksIn POST'13, LNCS 7796, pages 1-20. Springer, 2013. ( PDF | PDF (long version) | BibTeX + Abstract )
ACD12
M. Arapinis, V. Cheval and S. DelauneVerifying privacy-type properties in a modular wayIn 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 theoriesIn IJCAR'12, LNAI 7364, pages 164-178. Springer-Verlag, 2012. ( PDF | PDF (long version) | BibTeX + Abstract )
CDD12
V. Cortier, J. Degrieck and S. DelauneAnalysing routing protocols: four nodes topologies are sufficientIn POST'12, LNCS 7215, pages 30-50. Springer, 2012. ( PDF | PDF (long version) | BibTeX + Abstract )
DDS12
M. Dahl, S. Delaune and G. SteelFormal Analysis of Privacy for Anonymous Location Based ServicesIn TOSCA'11, LNCS 6993, pages 98-112. Springer, 2012. ( PDF | BibTeX + Abstract )
CDK11
C. Chevalier, S. Delaune and S. KremerTransforming Password Protocols to ComposeIn 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. DelauneTrace Equivalence Decision: Negative Tests and Non-determinismIn CCS'11, pages 321-330. ACM Press, 2011. ( PDF | BibTeX + Abstract )
ACD11a
M. Arnaud, V. Cortier and S. DelauneDeciding security for protocols with recursive testsIn CADE'11, LNAI, pages 49-63. Springer, 2011. ( PDF | PDF (long version) | BibTeX + Abstract )
DKRS11
S. Delaune, S. Kremer, M. D. Ryan and G. SteelFormal analysis of protocols based on TPM state registersIn CSF'11, pages 66-82. IEEE Computer Society Press, 2011. ( PDF | BibTeX + Abstract )
DDS10a
M. Dahl, S. Delaune and G. SteelFormal Analysis of Privacy for Vehicular Mix-ZonesIn 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. SteelA Formal Analysis of Authentication in the TPMIn FAST'10, LNCS 6561, pages 111-125. Springer, 2010. ( PDF | PS | PS.GZ | BibTeX + Abstract )
ACD10
M. Arnaud, V. Cortier and S. DelauneModeling and Verifying Ad Hoc Routing ProtocolsIn CSF'10, pages 59-74. IEEE Computer Society Press, 2010. ( PDF | PDF (long version) | BibTeX + Abstract )
CCD10
V. Cheval, H. Comon-Lundh and S. DelauneAutomating security analysis: symbolic equivalence of constraint systemsIn IJCAR'10, LNAI 6173, pages 412-426. Springer-Verlag, 2010. ( PDF | BibTeX + Abstract )
BDC09
S. Bursuc, S. Delaune and H. Comon-LundhDeducibility constraintsIn 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. PereiraSimulation based security in the applied pi calculusIn 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. KremerComputing knowledge in security protocols under convergent equational theoriesIn 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. DelauneA method for proving observational equivalenceIn 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. DelauneYAPA: A generic tool for computing intruder knowledgeIn 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. KremerEpistemic Logic for the Applied Pi CalculusIn FMOODS/FORTE'09, LNCS 5522, pages 182-197. Springer, 2009. ( PDF | PS | PS.GZ | BibTeX + Abstract )
ADK08
M. Arapinis, S. Delaune and S. KremerFrom One Session to Many: Dynamic Tags for Security ProtocolsIn LPAR'08, LNAI 5330, pages 128-142. Springer, 2008. ( PDF | PDF (long version) | BibTeX + Abstract )
DKR08
S. Delaune, S. Kremer and M. D. RyanComposition of Password-based ProtocolsIn CSF'08, pages 239-251. IEEE Computer Society Press, 2008. ( PDF | BibTeX + Abstract )
DKS08
S. Delaune, S. Kremer and G. SteelFormal Analysis of PKCS#11In 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. SmythAutomatic verification of privacy properties in the applied pi-calculusIn 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. DelauneSafely Composing Security ProtocolsIn FSTTCS'07, LNCS 4855, pages 352-363. Springer, 2007. ( PDF | PDF (long version) | BibTeX + Abstract )
DKR07a
S. Delaune, S. Kremer and M. D. RyanSymbolic Bisimulation for the Applied Pi-CalculusIn FSTTCS'07, LNCS 4855, pages 133-145. Springer, 2007. ( PDF | PDF (long version) | BibTeX + Abstract )
CD07a
V. Cortier and S. DelauneDeciding Knowledge in Security Protocols for Monoidal Equational TheoriesIn LPAR'07, LNAI 4790, pages 196-210. Springer, 2007. ( PDF | PS | PS.GZ | Slides | BibTeX + Abstract )
DLL07a
S. Delaune, H. Lin and Ch. LynchProtocol verification via rigid/flexible resolutionIn LPAR'07, LNAI 4790, pages 242-256. Springer, 2007. ( PDF | BibTeX + Abstract )
ACD07
M. Arnaud, V. Cortier and S. DelauneCombining algorithms for deciding knowledge in security protocolsIn 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. SteelA Formal Theory of Key ConjuringIn 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. DelauneDeducibility Constraints, Equational Theory and Electronic MoneyIn Rewriting, Computation and Proof, LNCS 4600, pages 196-212. Springer, 2007. ( PS | PS.GZ | BibTeX + Abstract )
BCD07b
S. Bursuc, H. Comon-Lundh and S. DelauneAssociative-Commutative Deducibility ConstraintsIn STACS'07, LNCS 4393, pages 634-645. Springer, 2007. ( PDF | PS | PS.GZ | BibTeX + Abstract )
DKR06a
S. Delaune, S. Kremer and M. D. RyanCoercion-Resistance and Receipt-Freeness in Electronic VotingIn 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. TreinenSymbolic Protocol Analysis in Presence of a Homomorphism Operator and Exclusive OrIn 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. DelauneThe finite variant property: How to get rid of some algebraic propertiesIn 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. JacquemardA Decision Procedure for the Verification of Security Protocols with Explicit DestructorsIn 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. JacquemardA Theory of Dictionary Attacks and its ComplexityIn 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. DelauneVerification 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. DelauneVé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

ACD11b
M. Arnaud, V. Cortier and S. DelauneModeling 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. SteelA 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. SteelFormal Analysis of Privacy for Vehicular Mix-ZonesIn FCS-PrivMod'10. 2010. ( PDF | PS | PS.GZ | BibTeX + Abstract )
CCD09
V. Cheval, H. Comon-Lundh and S. DelauneA decision procedure for proving observational equivalenceIn SecCo'09. 2009. ( PDF | BibTeX )
ACD09
M. Arnaud, V. Cortier and S. DelauneModeling and Verifying Ad Hoc Routing ProtocolIn SecReT'09, pages 33-46. 2009. ( PDF | PS | PS.GZ | BibTeX + Abstract )
CDK09c
Ş. Ciobâcă, S. Delaune and S. KremerComputing knowledge in security protocols under convergent equational theoriesIn SecReT'09, pages 47-58. 2009. ( PDF | BibTeX + Abstract )
DKR07b
S. Delaune, S. Kremer and M. D. RyanSymbolic bisimulation for the applied pi calculusIn SecCo'07. 2007. Preliminary version of [DKR07a]. ( PDF | PDF (long version) | BibTeX )
CD07b
V. Cortier and S. DelauneDeciding knowledge in security protocols for monoidal equational theoriesIn 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. LynchProtocol verification via rigid/flexible resolutionIn ADDCT'07, pages 2-16. 2007. Preliminary version of [DLL07a]. ( BibTeX + Abstract )
DKR06b
S. Delaune, S. Kremer and M. D. RyanVerifying Properties of Electronic Voting ProtocolsIn WOTE'06, pages 45-52. 2006. ( PDF | PS | PS.GZ | BibTeX + Abstract )
DKR05
S. Delaune, S. Kremer and M. D. RyanReceipt-Freeness: Formal Definition and Fault Attacks (Extended Abstract)In FEE 2005. 2005. Preliminary version of [DKR06a]. ( PDF | BibTeX )
DK04
S. Delaune and F. KlayVérification automatique appliquée à un protocole de commerce électroniqueIn JDIR'04, pages 260-269. 2004. ( PDF | Slides | BibTeX + Abstract )
DJ04c
S. Delaune and F. JacquemardNarrowing-Based Constraint Solving for the Verification of Security ProtocolsIn UNIF'04. 2004. Preliminary version of [DJ04a]. ( PS | PS.GZ | PS (long version) | PS.GZ (long version) | Slides | BibTeX + Abstract )
Del03a
S. DelauneIntruder Deduction Problem in Presence of Guessing AttacksIn SPV'03, pages 26-30. 2003. ( PDF | Slides | BibTeX + Abstract )
Del03b
S. DelauneVé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. DelauneUtilisation 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

DK13
S. Delaune and S. KremerDecision procedures for equivalence based properties, Deliverable VIP 3.1 (ANR-11-JS02-0006), 2013. 117 pages. ( PDF | PDF (long version) | BibTeX )
HD13
L. Hirschi and S. DelauneDescription of some case studies, Deliverable VIP 6.1, (ANR-11-JS02-0006), 2013. 14 pages. ( PDF | BibTeX )
CD13c
R. Chrétien and S. DelauneFormalising privacy-type security properties using the applied pi calculus, Deliverable VIP 1.1, (ANR-11-JS02-0006), 2013. 54 pages. ( PDF | BibTeX )
Del11b
S. DelauneAlgorithms for observational equivalence, Deliverable AVOTE 2.2, (ANR-07-SESU-002), 2011. 118 pages. ( PDF | BibTeX )
DK10
S. Delaune and S. KremerFormalising 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. KremerSpé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. KlaySynthè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. KremerRetour 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. KremerSpé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. VigneronRetour 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. TreinenSpé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. LafourcadeA 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

Search this list

Search the LSV database


highlight select


List of coauthors