Search Results

Documents authored by Delaune, Stéphanie

Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.29
A Symbolic Framework to Analyse Physical Proximity in Security Protocols

Authors: Alexandre Debant, Stéphanie Delaune, and Cyrille Wiedling

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
For many modern applications like e.g., contactless payment, and keyless systems, ensuring physical proximity is a security goal of paramount importance. Formal methods have proved their usefulness when analysing standard security protocols. However, existing results and tools do not apply to e.g., distance bounding protocols that aims to ensure physical proximity between two entities. This is due in particular to the fact that existing models do not represent in a faithful way the locations of the participants, and the fact that transmission of messages takes time. In this paper, we propose several reduction results: when looking for an attack, it is actually sufficient to consider a simple scenario involving at most four participants located at some specific locations. These reduction results allow one to use verification tools (e.g. ProVerif, Tamarin) developed for analysing more classical security properties. As an application, we analyse several distance bounding protocols, as well as a contactless payment protocol.
Cite as

Alexandre Debant, Stéphanie Delaune, and Cyrille Wiedling. A Symbolic Framework to Analyse Physical Proximity in Security Protocols. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{debant_et_al:LIPIcs.FSTTCS.2018.29,
  author =	{Debant, Alexandre and Delaune, St\'{e}phanie and Wiedling, Cyrille},
  title =	{{A Symbolic Framework to Analyse Physical Proximity in Security Protocols}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.29},
  URN =		{urn:nbn:de:0030-drops-99288},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.29},
  annote =	{Keywords: cryptographic protocols, verification, formal methods, process algebra, Dolev-Yao model}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2018.1
Analysing Privacy-Type Properties in Cryptographic Protocols (Invited Talk)

Authors: Stéphanie Delaune

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
Cryptographic protocols aim at securing communications over insecure networks such as the Internet, where dishonest users may listen to communications and interfere with them. For example, passports are no more pure paper documents. Instead, they contain a chip that stores additional information such as pictures and fingerprints of their holder. In order to ensure privacy, these chips include a mechanism, i.e. a cryptographic protocol, that does not let the passport disclose private information to external users except the intended terminal. This is just a single example but of course privacy appears in many other contexts such as RFIDs technologies or electronic voting. Formal methods have been successfully applied to automatically analyse traditional protocols and discover their flaws. Privacy-type security properties (e.g. anonymity, unlinkability, vote secrecy, ...) are expressed relying on a notion of behavioural equivalence, and are actually more difficult to analyse than confidentiality and authentication properties. We will discuss some recent advances that have been done to analyse automatically equivalence-based security properties, and we will review some issues that remain to be solved in this field.
Cite as

Stéphanie Delaune. Analysing Privacy-Type Properties in Cryptographic Protocols (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{delaune:LIPIcs.FSCD.2018.1,
  author =	{Delaune, St\'{e}phanie},
  title =	{{Analysing Privacy-Type Properties in Cryptographic Protocols}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{1:1--1:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.1},
  URN =		{urn:nbn:de:0030-drops-91715},
  doi =		{10.4230/LIPIcs.FSCD.2018.1},
  annote =	{Keywords: cryptographic protocols, symbolic models, privacy-related properties, behavioural equivalence}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.497
Partial Order Reduction for Security Protocols

Authors: David Baelde, Stéphanie Delaune, and Lucca Hirschi

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Security protocols are concurrent processes that communicate using cryptography with the aim of achieving various security properties. Recent work on their formal verification has brought procedures and tools for deciding trace equivalence properties (e.g. anonymity, unlinkability, vote secrecy) for a bounded number of sessions. However, these procedures are based on a naive symbolic exploration of all traces of the considered processes which, unsurprisingly, greatly limits the scalability and practical impact of the verification tools. In this paper, we mitigate this difficulty by developing partial order reduction techniques for the verification of security protocols. We provide reduced transition systems that optimally eliminate redundant traces, and which are adequate for model-checking trace equivalence properties of protocols by means of symbolic execution. We have implemented our reductions in the tool Apte, and demonstrated that it achieves the expected speedup on various protocols.
Cite as

David Baelde, Stéphanie Delaune, and Lucca Hirschi. Partial Order Reduction for Security Protocols. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 497-510, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{baelde_et_al:LIPIcs.CONCUR.2015.497,
  author =	{Baelde, David and Delaune, St\'{e}phanie and Hirschi, Lucca},
  title =	{{Partial Order Reduction for Security Protocols}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{497--510},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.497},
  URN =		{urn:nbn:de:0030-drops-53946},
  doi =		{10.4230/LIPIcs.CONCUR.2015.497},
  annote =	{Keywords: Cryptographic protocols, verification, process algebra, trace equivalence}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2011.204
Transforming Password Protocols to Compose

Authors: Céline Chevalier, Stéphanie Delaune, and Steve Kremer

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract
Formal, symbolic techniques are extremely useful for modelling and analysing security protocols. They improved our understanding of security protocols, allowed to discover flaws, and also provide support for protocol design. However, such analyses usually consider that the protocol is executed in isolation or assume a bounded number of protocol sessions. Hence, no security guarantee is provided when the protocol is executed in a more complex environment. In this paper, we study whether password protocols can be safely composed, even when a same password is reused. More precisely, we present a transformation which maps a password protocol that is secure for a single protocol session (a decidable problem) to a protocol that is secure for an unbounded number of sessions. Our result provides an effective strategy to design secure password protocols: (i) design a protocol intended to be secure for one protocol session; (ii) apply our transformation and obtain a protocol which is secure for an unbounded number of sessions. Our technique also applies to compose different password protocols allowing us to obtain both inter-protocol and inter-session composition.
Cite as

Céline Chevalier, Stéphanie Delaune, and Steve Kremer. Transforming Password Protocols to Compose. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 204-216, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{chevalier_et_al:LIPIcs.FSTTCS.2011.204,
  author =	{Chevalier, C\'{e}line and Delaune, St\'{e}phanie and Kremer, Steve},
  title =	{{Transforming Password Protocols to Compose}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{204--216},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.204},
  URN =		{urn:nbn:de:0030-drops-33273},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.204},
  annote =	{Keywords: Security, cryptographic protocols, composition}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2316
Simulation based security in the applied pi calculus

Authors: Stéphanie Delaune, Steve Kremer, and Olivier Pereira

Published in: LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

Abstract
We present a symbolic framework for refinement and composition of security protocols. The framework uses the notion of ideal functionalities. These are abstract systems which are secure by construction and which can be combined into larger systems. They can be separately refined in order to obtain concrete protocols implementing them. Our work builds on ideas from the ``trusted party paradigm'' used in computational cryptography models. The underlying language we use is the applied pi calculus which is a general language for specifying security protocols. In our framework we can express the different standard flavours of simulation-based security which happen to all coincide. We illustrate our framework on an authentication functionality which can be realized using the Needham-Schroeder-Lowe protocol. For this we need to define an ideal functionality for asymmetric encryption and its realization. We show a joint state result for this functionality which allows composition (even though the same key material is reused) using a tagging mechanism.
Cite as

Stéphanie Delaune, Steve Kremer, and Olivier Pereira. Simulation based security in the applied pi calculus. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 169-180, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{delaune_et_al:LIPIcs.FSTTCS.2009.2316,
  author =	{Delaune, St\'{e}phanie and Kremer, Steve and Pereira, Olivier},
  title =	{{Simulation based security in the applied pi calculus}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{169--180},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2316},
  URN =		{urn:nbn:de:0030-drops-23163},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2316},
  annote =	{Keywords: Simulation based security, applied pi calculus, joint state theorem, authentication protocols}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact