5 Search Results for "Cortier, Véronique"

Document
DOI: 10.4230/LIPIcs.CONCUR.2020.31
Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions

Authors: Emanuele D'Osualdo and Felix Stutz

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
We develop a theory of decidable inductive invariants for an infinite-state variant of the Applied πcalc, with applications to automatic verification of stateful cryptographic protocols with unbounded sessions/nonces. Since the problem is undecidable in general, we introduce depth-bounded protocols, a strict generalisation of a class from the literature, for which our decidable analysis is sound and complete. Our core contribution is a procedure to check that an invariant is inductive, which implies that every reachable configuration satisfies it. Our invariants can capture security properties like secrecy, can be inferred automatically, and represent an independently checkable certificate of correctness. We provide a prototype implementation and we report on its performance on some textbook examples.
Cite as

Emanuele D'Osualdo and Felix Stutz. Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 31:1-31:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{dosualdo_et_al:LIPIcs.CONCUR.2020.31,
  author =	{D'Osualdo, Emanuele and Stutz, Felix},
  title =	{{Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{31:1--31:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.31},
  URN =		{urn:nbn:de:0030-drops-128433},
  doi =		{10.4230/LIPIcs.CONCUR.2020.31},
  annote =	{Keywords: Security Protocols, Infinite-State Verification, Ideal Completions for WSTS}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2020.1
Verification of Security Protocols (Invited Talk)

Authors: Véronique Cortier

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
Cryptographic protocols aim at securing communications over insecure networks like the Internet. Over the past decades, numerous decision procedures and tools have been developed to automatically analyse the security of protocols. The field has now reached a good level of maturity with efficient techniques for the automatic security analysis of protocols After an overview of some famous protocols and flaws, we will describe the current techniques for security protocols analysis, often based on logic, and review the key challenges towards a fully automated verification.
Cite as

Véronique Cortier. Verification of Security Protocols (Invited Talk). In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cortier:LIPIcs.CSL.2020.1,
  author =	{Cortier, V\'{e}ronique},
  title =	{{Verification of Security Protocols}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.1},
  URN =		{urn:nbn:de:0030-drops-116447},
  doi =		{10.4230/LIPIcs.CSL.2020.1},
  annote =	{Keywords: Security protocols, automated deduction, security}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.575
Secure Refinements of Communication Channels

Authors: Vincent Cheval, Véronique Cortier, and Eric le Morvan

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
It is a common practice to design a protocol (say Q) assuming some secure channels. Then the secure channels are implemented using any standard protocol, e.g. TLS. In this paper, we study when such a practice is indeed secure. We provide a characterization of both confidential and authenticated channels. As an application, we study several protocols of the literature including TLS and BAC protocols. Thanks to our result, we can consider a larger number of sessions when analyzing complex protocols resulting from explicit implementation of the secure channels of some more abstract protocol Q.
Cite as

Vincent Cheval, Véronique Cortier, and Eric le Morvan. Secure Refinements of Communication Channels. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 575-589, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cheval_et_al:LIPIcs.FSTTCS.2015.575,
  author =	{Cheval, Vincent and Cortier, V\'{e}ronique and le Morvan, Eric},
  title =	{{Secure Refinements of Communication Channels}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{575--589},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.575},
  URN =		{urn:nbn:de:0030-drops-56583},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.575},
  annote =	{Keywords: Protocol, Composition, Formal methods, Channels, Implementation}
}
Document
DOI: 10.4230/LIPIcs.STACS.2011.29
How to prove security of communication protocols? A discussion on the soundness of formal models w.r.t. computational ones.

Authors: Hubert Comon-Lundh and Véronique Cortier

Published in: LIPIcs, Volume 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)

Abstract
Security protocols are short programs that aim at securing communication over a public network. Their design is known to be error-prone with flaws found years later. That is why they deserve a careful security analysis, with rigorous proofs. Two main lines of research have been (independently) developed to analyse the security of protocols. On the one hand, formal methods provide with symbolic models and often automatic proofs. On the other hand, cryptographic models propose a tighter modeling but proofs are more difficult to write and to check. An approach developed during the last decade consists in bridging the two approaches, showing that symbolic models are sound w.r.t. symbolic ones, yielding strong security guarantees using automatic tools. These results have been developed for several cryptographic primitives (e.g. symmetric and asymmetric encryption, signatures, hash) and security properties. While proving soundness of symbolic models is a very promising approach, several technical details are often not satisfactory. Focusing on symmetric encryption, we describe the difficulties and limitations of the available results.
Cite as

Hubert Comon-Lundh and Véronique Cortier. How to prove security of communication protocols? A discussion on the soundness of formal models w.r.t. computational ones.. In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 9, pp. 29-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{comonlundh_et_al:LIPIcs.STACS.2011.29,
  author =	{Comon-Lundh, Hubert and Cortier, V\'{e}ronique},
  title =	{{How to prove security of communication protocols? A discussion on the soundness of formal models w.r.t. computational ones.}},
  booktitle =	{28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)},
  pages =	{29--44},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-25-5},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{9},
  editor =	{Schwentick, Thomas and D\"{u}rr, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2011.29},
  URN =		{urn:nbn:de:0030-drops-29993},
  doi =		{10.4230/LIPIcs.STACS.2011.29},
  annote =	{Keywords: verification, security, cryptography}
}
Document
DOI: 10.4230/OASIcs.TrustworthySW.2006.691
Relating two standard notions of secrecy

Authors: Eugen Zalinescu, Véronique Cortier, and Michaël Rusinowitch

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)

Abstract
Two styles of definitions are usually considered to express that a security protocol preserves the confidentiality of a data { t s}. Reach-ability-based secrecy means that { t s} should never be disclosed while equi-valence-based secrecy states that two executions of a protocol with distinct instances for { t s} should be indistinguishable to an attacker. Although the second formulation ensures a higher level of security and is closer to cryptographic notions of secrecy, decidability results and automatic tools have mainly focused on the first definition so far. This paper initiates a systematic investigation of situations where syntactic secrecy entails strong secrecy. We show that in the passive case, reachability-based secrecy actually implies equivalence-based secrecy for signatures, symmetric and asymmetric encryption provided that the primitives are probabilistic. For active adversaries in the case of symmetric encryption, we provide sufficient (and rather tight) conditions on the protocol for this implication to hold.
Cite as

Eugen Zalinescu, Véronique Cortier, and Michaël Rusinowitch. Relating two standard notions of secrecy. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{zalinescu_et_al:OASIcs.TrustworthySW.2006.691,
  author =	{Zalinescu, Eugen and Cortier, V\'{e}ronique and Rusinowitch, Micha\"{e}l},
  title =	{{Relating two standard notions of secrecy}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--29},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.691},
  URN =		{urn:nbn:de:0030-drops-6911},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.691},
  annote =	{Keywords: Verification, security protocols, secrecy, applied-pi calculus}
}
  • Refine by Author
  • 4 Cortier, Véronique
  • 1 Cheval, Vincent
  • 1 Comon-Lundh, Hubert
  • 1 D'Osualdo, Emanuele
  • 1 Rusinowitch, Michaël
  • Show More...

  • Refine by Classification
  • 1 Security and privacy → Formal security models
  • 1 Theory of computation → Program verification

  • Refine by Keyword
  • 2 security
  • 1 Channels
  • 1 Composition
  • 1 Formal methods
  • 1 Ideal Completions for WSTS
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 2 2020
  • 1 2006
  • 1 2011
  • 1 2015

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 Imprint Privacy Contact