DROPS

Document

Invited Paper

DOI: 10.4230/LIPIcs.LICS.2026.2

Formal Verification of Security Protocols: 25 Years of ProVerif (Invited Paper)

Authors: Stéphanie Delaune

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract

Cryptographic protocols are essential to secure communication but remain difficult to design correctly, motivating the need for rigorous verification methods. This paper provides a brief overview of symbolic verification techniques, focusing on the evolution and impact of the tool ProVerif over the past 25 years. We discuss its core principles, key extensions for richer security properties, and recent work on handling algebraic theories such as exclusive-or (XOR). We conclude by highlighting ongoing challenges, including usability and interoperability between verification approaches.

Cite as

Stéphanie Delaune. Formal Verification of Security Protocols: 25 Years of ProVerif (Invited Paper). In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 2:1-2:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{delaune:LIPIcs.LICS.2026.2,
  author =	{Delaune, St\'{e}phanie},
  title =	{{Formal Verification of Security Protocols: 25 Years of ProVerif}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{2:1--2:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.2},
  URN =		{urn:nbn:de:0030-drops-267890},
  doi =		{10.4230/LIPIcs.LICS.2026.2},
  annote =	{Keywords: Security protocols, Formal verification}
}

Document

DOI: 10.4230/LIPIcs.AFT.2025.5

Blockchain Governance via Sharp Anonymous Multisignatures

Authors: Wonseok Choi, Xiangyu Liu, and Vassilis Zikas

Published in: LIPIcs, Volume 354, 7th Conference on Advances in Financial Technologies (AFT 2025)

Abstract

Electronic voting has occupied a large part of the cryptographic protocols literature. The recent reality of blockchains - in particular, their need for online governance mechanisms - has brought new parameters and requirements to the problem. We identify the key requirements of a blockchain governance mechanism, namely correctness (including eliminative double votes), voter anonymity, and traceability, and investigate mechanisms that can achieve them with minimal interaction and under assumptions that fit the blockchain setting. First, we define a signature-like primitive, which we term sharp anonymous multisignatures (in short, ♯AMS) that tightly meets the needs of blockchain governance. In a nutshell, ♯AMSs allow any set of parties to generate a signature, e.g., on a proposal to be voted upon, which, if posted on the blockchain, hides the identities of the signers/voters but reveals their number. This can be seen as a (strict) generalization of threshold ring signatures (TRS). We next turn to constructing such ♯AMSs and using them in various governance scenarios - e.g., single vote vs. multiple votes per voter. In this direction, although the definition of TRS does not imply ♯AMS, one can compile some existing TRS constructions into ♯AMS. This raises the question: What is the TRS structure that allows such a compilation? To answer the above, we devise templates for TRSs. Our templates encapsulate and abstract the structure that allows for the above compilation - most of the TRS schemes that can be compiled into ♯AMS are, in fact, instantiations of our template. This abstraction makes our template generic for instantiating TRSs and ♯AMSs from different cryptographic assumptions (e.g., DDH, LWE, etc.). One of our templates is based on chameleon hashes, and we explore a framework of lossy chameleon hashes to understand their nature fully. Finally, we turn to how ♯AMS schemes can be used in our applications. We provide fast (in some cases non-interactive) ♯AMS-based blockchain governance mechanisms for a wide spectrum of assumptions on the honesty (semi-honest vs malicious) and availability of voters and proposers.

Cite as

Wonseok Choi, Xiangyu Liu, and Vassilis Zikas. Blockchain Governance via Sharp Anonymous Multisignatures. In 7th Conference on Advances in Financial Technologies (AFT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 354, pp. 5:1-5:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{choi_et_al:LIPIcs.AFT.2025.5,
  author =	{Choi, Wonseok and Liu, Xiangyu and Zikas, Vassilis},
  title =	{{Blockchain Governance via Sharp Anonymous Multisignatures}},
  booktitle =	{7th Conference on Advances in Financial Technologies (AFT 2025)},
  pages =	{5:1--5:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-400-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{354},
  editor =	{Avarikioti, Zeta and Christin, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2025.5},
  URN =		{urn:nbn:de:0030-drops-247242},
  doi =		{10.4230/LIPIcs.AFT.2025.5},
  annote =	{Keywords: Blockchain, E-voting, Threshold Ring Signatures, Threshold Cryptography}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2025.30

Open Bisimilarity for the π-Calculus with Mismatch

Authors: Tiange Liu, Alwen Tiu, and Ross Horne

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract

Open bisimilarity is an equivalence relation for the π-calculus that is also congruence, making it suitable to use in compositional reasoning for mobile processes and communication protocols. The original definition of open bisimilarity, due to Sangiorgi, does not account for the mismatch operator, that is crucial in modelling real-world protocols. When mismatch is present, the congruence property no longer holds for open bisimilarity. In a LICS 2018 paper, Horne et al. proposed an extension of open bisimilarity, using a history-indexed class of relations, to address this problem. That definition, however, turns out to be non-compositional as we shall demonstrate in this paper. This paper presents a new definition of open bisimilarity in the π-calculus that incorporates mismatch. This is achieved by augmenting the transition semantics of the π-calculus with an explicit assumption about name distinctions, and by requiring that open bisimulation to be closed under an arbitary extension of the name distinctions assumption. We then prove that the resulting open bisimilarity is both an equivalence relation and a congruence.

Cite as

Tiange Liu, Alwen Tiu, and Ross Horne. Open Bisimilarity for the π-Calculus with Mismatch. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{liu_et_al:LIPIcs.CONCUR.2025.30,
  author =	{Liu, Tiange and Tiu, Alwen and Horne, Ross},
  title =	{{Open Bisimilarity for the \pi-Calculus with Mismatch}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{30:1--30:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.30},
  URN =		{urn:nbn:de:0030-drops-239805},
  doi =		{10.4230/LIPIcs.CONCUR.2025.30},
  annote =	{Keywords: mismatch, open bisimilarity, pi calculus}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2025.18

Knowledge Problems vs Unification and Matching: Dichotomy Results

Authors: Serdar Erbatur, Andrew M. Marshall, Paliath Narendran, and Christophe Ringeissen

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract

The research area of cryptographic protocol analysis contains a number of innovative algorithms and procedures for checking various security properties of protocols. Most of these procedures focus on solving one of several "knowledge problems" that model intruder knowledge. Solving these problems can demonstrate the ability of the intruder to obtain some forbidden information of the protocol, such as secret keys. Two important examples of these problems are the deduction problem and the static equivalence problem. Deduction is concerned with the ability to derive a term from a set of terms (or knowledge) obtained from the observation of a protocol instance. Static equivalence, on the other hand, is concerned with distinguishing between two runs of a protocol based on two sets of knowledge. These two knowledge problems at first inspection appear to be very close to the older automated reasoning problems of matching and unification. However, this first impression is wrong, and there have been a few results that have shown theories where one problem, such as unification, is undecidable but another problem, such as deduction, is decidable. These existing dichotomy results were, however, incomplete, and not all cases had been examined, thus leaving the possibility of some connection between the problems for those unexamined cases. In this paper, we consider the missing dichotomy cases. For each of the remaining cases, we demonstrate a theory that separates the two problems. In addition, once the dichotomy results are completed, it leaves open the question of the existence of non-trivial classes of theories for which all four of the problems are decidable. One example for which this is true is the well-known class of subterm convergent term rewrite systems. In this paper, we develop another example, a class of restrictive permutative theories for which all problems are likewise decidable.

Cite as

Serdar Erbatur, Andrew M. Marshall, Paliath Narendran, and Christophe Ringeissen. Knowledge Problems vs Unification and Matching: Dichotomy Results. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{erbatur_et_al:LIPIcs.FSCD.2025.18,
  author =	{Erbatur, Serdar and Marshall, Andrew M. and Narendran, Paliath and Ringeissen, Christophe},
  title =	{{Knowledge Problems vs Unification and Matching: Dichotomy Results}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.18},
  URN =		{urn:nbn:de:0030-drops-236331},
  doi =		{10.4230/LIPIcs.FSCD.2025.18},
  annote =	{Keywords: Knowledge Problems, Unification, Matching, Decidability}
}

Document

DOI: 10.4230/LIPIcs.CSL.2025.24

Propositional Logics of Overwhelming Truth

Authors: Thibaut Antoine and David Baelde

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract

Cryptographers consider that asymptotic security holds when, for any possible attacker running in polynomial time, the probability that the attack succeeds is negligible, i.e. that it tends fast enough to zero with the size of secrets. In order to reason formally about cryptographic truth, one may thus consider logics where a formula is satisfied when it is true with overwhelming probability, i.e. a probability that tends fast enough to one with the size of secrets. In such logics it is not always the case that either ϕ or ⌝ϕ is satisfied by a given model. However, security analyses will inevitably involve specific formulas, which we call determined, satisfying this property - typically because they are not probabilistic. The Squirrel proof assistant, which implements a logic of overwhelming truth, features ad-hoc proof rules for this purpose. In this paper, we study several propositional logics whose semantics rely on overwhelming truth. We first consider a modal logic of overwhelming truth, and show that it coincides with S5. In addition to providing an axiomatization, this brings a well-behaved proof system for our logic in the form of Poggiolesi’s hypersequent calculus. Further, we show that this system can be adapted to elegantly incorporate reasoning on determined atoms. We then consider a logic that is closer to Squirrel’s language, where the overwhelming truth modality cannot be nested. In that case, we show that a simple proof system, based on regular sequents, is sound and complete. This result justifies the core of Squirrel’s proof system.

Cite as

Thibaut Antoine and David Baelde. Propositional Logics of Overwhelming Truth. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{antoine_et_al:LIPIcs.CSL.2025.24,
  author =	{Antoine, Thibaut and Baelde, David},
  title =	{{Propositional Logics of Overwhelming Truth}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.24},
  URN =		{urn:nbn:de:0030-drops-227818},
  doi =		{10.4230/LIPIcs.CSL.2025.24},
  annote =	{Keywords: Cryptography, Modal Logic, Sequent Calculus}
}

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}
}

10 Search Results for "Delaune, Stéphanie"

Formal Verification of Security Protocols: 25 Years of ProVerif (Invited Paper)

Abstract

Cite as

Blockchain Governance via Sharp Anonymous Multisignatures

Abstract

Cite as

Open Bisimilarity for the π-Calculus with Mismatch

Abstract

Cite as

Knowledge Problems vs Unification and Matching: Dichotomy Results

Abstract

Cite as

Propositional Logics of Overwhelming Truth

Abstract

Cite as

A Symbolic Framework to Analyse Physical Proximity in Security Protocols

Abstract

Cite as

Analysing Privacy-Type Properties in Cryptographic Protocols (Invited Talk)

Abstract

Cite as

Partial Order Reduction for Security Protocols

Abstract

Cite as

Transforming Password Protocols to Compose

Abstract

Cite as

Simulation based security in the applied pi calculus

Abstract

Cite as

Thanks for your feedback!

Could not send message