@inproceedings{baelde12itp, address = {Princeton, New~Jersey, USA}, year = 2012, month = aug, volume = 7406, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Beringer, Lennart and Felty, Amy P.}, acronym = {{ITP}'12}, booktitle = {{P}roceedings of the {T}hird {I}nternational {C}onference on {I}nteractive {T}heorem {P}roving ({ITP}'12)}, author = {Baelde, David and Courtieu, Pierre and Gross{-}Amblard, David and Paulin{-}Mohring, {\relax Ch}ristine}, title = {Towards Provably Robust Watermarking}, pages = {201-216}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde12itp.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde12itp.pdf}, doi = {10.1007/978-3-642-32347-8_14}, abstract = {Watermarking techniques are used to help identifying copies of publicly released information. They consist in applying a slight and secret modification to the data before its release, in a way that should be \emph{robust}, i.e., remain recognizable even in (reasonably) modified copies of the data. In~this paper, we present new results about the robustness of watermarking schemes against arbitrary attackers, and the formalization of those results in \textsc{Coq}. We used the \textsc{Alea} library, which formalizes probability theory and models probabilistic programs using a simple monadic translation. This work illustrates the strengths and particularities of the induced style of reasoning about probabilistic programs. Our technique for proving robustness is adapted from methods commonly used for cryptographic protocols, and we discuss its relevance to the field of watermarking.} }

@inproceedings{baelde12lics, address = {Dubrovnik, Croatia}, month = jun, year = 2012, publisher = {{IEEE} Computer Society Press}, acronym = {{LICS}'12}, booktitle = {{P}roceedings of the 27th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'12)}, author = {Baelde, David and Nadathur, Gopalan}, title = {Combining Deduction Modulo and Logics of Fixed-Point Definitions}, pages = {105-114}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde12lics.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde12lics.pdf}, doi = {10.1109/LICS.2012.22}, abstract = {Inductive and coinductive specifications are widely used in formalizing computational systems. Such specifications have a natural rendition in logics that support fixed-point definitions. Another useful formalization device is that of recursive specifications. These specifications are not directly complemented by fixed-point reasoning techniques and, correspondingly, do not have to satisfy strong monotonicity restrictions. We show how to incorporate a rewriting capability into logics of fixed-point definitions towards additionally supporting recursive specifications. In particular, we describe a natural deduction calculus that adds a form of {"}closed-world{"} equality---a key ingredient to supporting fixed-point definitions----to \emph{deduction modulo}, a framework for extending a logic with a rewriting layer operating on formulas. We show that our calculus enjoys strong normalizability when the rewrite system satisfies general properties and we demonstrate its usefulness in specifying and reasoning about syntax-based descriptions. The integration of closed-world equality into deduction modulo leads us to reconfigure the elimination principle for this form of equality in a way that resolves long-standing issues concerning the stability of finite proofs under proof reduction.} }

@article{baelde12tocl, publisher = {ACM Press}, journal = {ACM Transactions on Computational Logic}, author = {Baelde, David}, title = {Least and greatest fixed points in linear logic}, month = jan, year = {2012}, volume = {13}, number = {1}, nopages = {}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde12tocl.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde12tocl.pdf}, doi = {10.1145/2071368.2071370}, abstract = {The first-order theory of MALL (multiplicative, additive linear logic) over only equalities is a well-structured but weak logic since it cannot capture unbounded (infinite) behavior. Instead of accounting for unbounded behavior via the addition of the exponentials (! and ?), we add least and greatest fixed point operators. The resulting logic, which we call \(\mu\)MALL, satisfies two fundamental proof theoretic properties: we establish weak normalization for it, and we design a focused proof system that we prove complete with respect to the initial system. That second result provides a strong normal form for cut-free proof structures that can be used, for example, to help automate proof search. We show how these foundations can be applied to intuitionistic logic.} }

@inproceedings{snow10ppdp, address = {Hagenberg, Austria}, month = jul, year = 2010, publisher = {ACM Press}, editor = {Kutsia, Temur and Schreiner, Wolfgang and Fern{\'a}ndez, Maribel}, acronym = {{PPDP}'10}, booktitle = {{P}roceedings of the 12th {I}nternational {ACM} {SIGPLAN} {C}onference on {P}rinciples and {P}ractice of {D}eclarative {P}rogramming ({PPDP}'10)}, author = {Snow, Zachary and Baelde, David and Nadathur, Gopalan}, title = {A Meta-Programming Approach to Realizing Dependently Typed Logic Programming}, pages = {187-198}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/snow10ppdp.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/snow10ppdp.pdf}, doi = {10.1145/1836089.1836113}, abstract = {Dependently typed lambda calculi such as the Logical Framework (LF) can encode relationships between terms in types and can naturally capture correspondences between formulas and their proofs. Such calculi can also be given a logic programming interpretation: the Twelf system is based on such an interpretation of LF. We consider here whether a conventional logic programming language can provide the benefits of a Twelf-like system for encoding type and proof-and-formula dependencies. In particular, we present a simple mapping from LF specifications to a set of formulas in the higher-order hereditary Harrop (\emph{hohh}) language, that relates derivations and proof-search between the two frameworks. We then show that this encoding can be improved by exploiting knowledge of the well-formedness of the original LF specifications to elide much redundant type-checking information. The resulting logic program has a structure that closely resembles the original specification, thereby allowing LF specifications to be viewed as \emph{hohh} meta-programs. Using the Teyjus implementation of \(\lambda\)Prolog, we show that our translation provides an efficient means for executing LF specifications, complementing the ability that the Twelf system provides for reasoning about them.} }

@inproceedings{baelde07cade, address = {Bremen, Germany}, month = jul, year = 2007, volume = 4603, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Pfenning, Frank}, acronym = {{CADE}'07}, booktitle = {{P}roceedings of the 21st {I}nternational {C}onference on {A}utomated {D}eduction ({CADE}'07)}, author = {Baelde, David and Gacek, Andrew and Miller, Dale and Nadathur, Gopalan and Tiu, Alwen}, title = {The {B}edwyr system for model checking over syntactic expressions}, pages = {391-397}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde07cade.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde07cade.pdf}, doi = {10.1007/978-3-540-73595-3_28}, abstract = {Bedwyr is a generalization of logic programming that allows model checking directly on syntactic expressions possibly containing bindings. This system, written in OCaml, is a direct implementation of two recent advances in the theory of proof search. The first is centered on the fact that both finite success and finite failure can be captured in the sequent calculus by incorporating inference rules for \emph{definitions} that allow \emph{fixed points} to be explored. As a result, proof search in such a sequent calculus can capture simple model checking problems as well as may and must behavior in operational semantics. The second is that higher-order abstract syntax is directly supported using term-level \(\lambda\)-binders and the quantifier known as~\(\nabla\). These features allow reasoning directly on expressions containing bound variables.} }

@inproceedings{baelde07lpar, address = {Yerevan, Armenia}, month = oct, year = 2007, volume = 4790, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Dershowitz, Nachum and Voronkov, Andrei}, acronym = {{LPAR}'07}, booktitle = {{P}roceedings of the 14th {I}nternational {C}onference on {L}ogic for {P}rogramming, {A}rtificial {I}ntelligence, and {R}easoning ({LPAR}'07)}, author = {Baelde, David and Miller, Dale}, title = {Least and greatest fixed points in linear logic}, pages = {92-106}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde07lpar.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde07lpar.pdf}, doi = {10.1007/978-3-540-75560-9_9}, abstract = {The first-order theory of MALL (multiplicative, additive linear logic) over only equalities is an interesting but weak logic since it cannot capture un- bounded (infinite) behavior. Instead of accounting for unbounded behavior via the addition of the exponentials (! and ?), we add least and greatest fixed point operators. The resulting logic, which we call \(\mu\)MALL\textsuperscript{=} , satisfies two fundamental proof theoretic properties. In particular, \(\mu\)MALL\textsuperscript{=} satisfies cut-elimination, which implies consistency, and has a complete focused proof system. This second result about focused proofs provides a strong normal form for cut-free proof structures that can be used, for example, to help automate proof search. We then consider applying these two results about \(\mu\)MALL\textsuperscript{=} to derive a focused proof system for an intuitionistic logic extended with induction and co-induction. The traditional approach to encoding intuitionistic logic into linear logic relies heavily on using the exponentials, which unfortunately weaken the focusing discipline. We get a better focused proof system by observing that certain fixed points satisfy the structural rules of weakening and contraction (without using exponentials). The resulting focused proof system for intuitionistic logic is closely related to the one implemented in Bedwyr, a recent model checker based on logic programming. We discuss how our proof theory might be used to build a computational system that can partially automate induction and co-induction.} }

@inproceedings{baelde08jfla, address = {{\'E}tretat, France}, month = jan, year = 2008, publisher = {INRIA}, editor = {Blazy, Sandrine}, acronym = {{JFLA}'08}, booktitle = {{A}ctes des 19{\`e}mes {J}ourn{\'e}es {F}rancophones sur les {L}angages {A}pplicatifs ({JFLA}'08)}, author = {Baelde, David and Mimram, Samuel}, title = {{De la webradio lambda \`a la {{\(\lambda\)}}-webradio}}, pages = {47-61}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde08jfla.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde08jfla.pdf} }

@inproceedings{baelde08lfmtp, address = {Pittsburgh, Pennsylvania, USA}, month = jan, year = 2009, volume = 228, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Abel, Andreas and Urban, Christian}, acronym = {{LFMTP}'08}, booktitle = {{I}nternational {W}orkshop on {L}ogical {F}rameworks and {M}eta-{L}anguages: {T}heory and {P}ractice ({LFMTP}'08)}, author = {Baelde, David}, title = {On the Expressivity of Minimal Generic Quantification}, pages = {3-19}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde08lfmtp.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde08lfmtp.pdf}, doi = {10.1016/j.entcs.2008.12.113}, abstract = {We come back to the initial design of the \(\nabla\) quantifier by Miller and Tiu, which we call minimal generic quantification. In the absence of fixed points, it is equivalent to seemingly stronger designs. However, several expected theorems about (co)inductive specifications can not be derived in that setting. We present a refinement of minimal generic quantification that brings the expected expressivity while keeping the minimal semantic, which we claim is useful to get natural adequate specifications. We build on the idea that generic quantification is not a logical connective but one that is defined, like negation in classical logics. This allows us to use the standard (co)induction rule, but obtain much more expressivity than before. We show classes of theorems that can now be derived in the logic, and present a few practical examples.} }

@inproceedings{baelde09tableaux, address = {Oslo, Norway}, month = jul, year = 2009, volume = 5607, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, editor = {Giese, Martin and Waaler, Arild}, acronym = {{TABLEAUX}'09}, booktitle = {{P}roceedings of the 18th {I}nternational {W}orkshop on {T}heorem {P}roving with {A}nalytic {T}ableaux and {R}elated {M}ethods ({TABLEAUX}'09)}, author = {Baelde, David}, title = {On the proof theory of regular fixed points}, pages = {93-107}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde09tableaux.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde09tableaux.pdf}, doi = {10.1007/978-3-642-02716-1_8}, abstract = {We consider encoding finite automata as least fixed points in a proof-theoretical framework equipped with a general induction scheme, and study automata inclusion in that setting. We provide a coinductive characterization of inclusion that yields a natural bridge to proof-theory. This leads us to generalize these observations to \emph{regular formulas}, obtaining new insights about inductive theorem proving and cyclic proofs in particular. } }

@inproceedings{baelde10ijcar, address = {Edinburgh, Scotland, UK}, month = jul, year = 2010, volume = {6173}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer-Verlag}, editor = {Giesl, J{\"u}rgen and Haehnle, Reiner}, acronym = {{IJCAR}'10}, booktitle = {{P}roceedings of the 5th {I}nternational {J}oint {C}onference on {A}utomated {R}easoning ({IJCAR}'10)}, author = {Baelde, David and Miller, Dale and Snow, Zachary}, title = {Focused Inductive Theorem Proving}, pages = {278-292}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde10ijcar.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde10ijcar.pdf}, doi = {10.1007/978-3-642-14203-1_24}, abstract = {\emph{Focused proof systems} provide means for reducing and structuring the non-determinism involved in searching for sequent calculus proofs. We present a focused proof system for a first-order logic with inductive and co-inductive definitions in which the introduction rules are partitioned into an asynchronous phase and a synchronous phase. These focused proofs allow us to naturally see proof search as being organized around interleaving intervals of computation and more general deduction. For example, entire Prolog-like computations can be captured using a single synchronous phase and many model-checking queries can be captured using an asynchronous phase followed by a synchronous phase. Leveraging these ideas, we have developed an interactive proof assistant, called Tac, for this logic. We describe its high-level design and illustrate how it is capable of automatically proving many theorems using induction and coinduction. Since the automatic proof procedure is structured using focused proofs, its behavior is often rather easy to anticipate and modify. We illustrate the strength of Tac with several examples of proved theorems, some achieved entirely automatically and others achieved with user guidance.} }

@inproceedings{baelde11sofsem, address = {Nov{\'y} Smokovec, Slovakia}, month = jan, year = 2011, volume = 6543, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Cern{\'a}, Ivana and Gyim{\'o}thy, Tibor and Hromkovic, Juraj and Jeffery, Keith G. and Kr{\'a}lovic, Rastislav and Vukoli{\'c}, Marko and Wolf, Stefan}, acronym = {{SOFSEM}'11}, booktitle = {{P}roceedings of the 37th International Conference on Current Trends in Theory and Practice of Computer Science ({SOFSEM}'11)}, author = {Baelde, David and Beauxis, Romain and Mimram, Samuel}, title = {Liquidsoap: a~High-Level Programming Language for Multimedia Streaming}, pages = {99-110}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde11sofsem.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/baelde11sofsem.pdf}, doi = {10.1007/978-3-642-18381-2_8}, abstract = {Generating multimedia streams, such as in a netradio, is a task which is complex and difficult to adapt to every users' needs. We introduce a novel approach in order to achieve it, based on a dedicated high-level functional programming language, called \emph{Liquidsoap}, for generating, manipulating and broadcasting multimedia streams. Unlike traditional approaches, which are based on configuration files or static graphical interfaces, it also allows the user to build complex and highly customized systems. This language is based on a model for streams and contains operators and constructions, which make it adapted to the generation of streams. The interpreter of the language also ensures many properties concerning the good execution of the stream generation.} }

@inproceedings{BDH-post14, address = {Grenoble, France}, month = apr, year = 2014, volume = {8414}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Abadi, Mart{\'\i}n and Kremer, Steve}, acronym = {{POST}'14}, booktitle = {{P}roceedings of the 3rd {I}nternational {C}onference on {P}rinciples of {S}ecurity and {T}rust ({POST}'14)}, author = {Baelde, David and Delaune, St{\'e}phanie and Hirschi, Lucca}, title = {A~reduced semantics for deciding trace equivalence using constraint systems}, pages = {1-21}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDH-post14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDH-post14.pdf}, doi = {10.1007/978-3-642-54792-8_1}, abstract = {Many privacy-type properties of security protocols can be modelled using trace equivalence properties in suitable process algebras. It has been shown that such properties can be decided for interesting classes of finite processes (i.e.,~without replication) by means of symbolic execution and constraint solving. However, this does not suffice to obtain practical tools. Current prototypes suffer from a classical combinatorial explosion problem caused by the exploration of many interleavings in the behaviour of processes. Modersheim et~al. have tackled this problem for reachability properties using partial order reduction techniques. We revisit their work, generalize it and adapt it for equivalence checking. We obtain an optimization in the form of a reduced symbolic semantics that eliminates redundant interleavings on the fly.} }

@article{BCGMNTW-jfr14, publisher = {University of Bologna}, journal = {Journal of Formalized Reasoning}, author = {Baelde, David and Chaudhuri, Kaustuv and Gacek, Andrew and Miller, Dale and Nadathur, Gopalan and Tiu, Alwen and Wang, Yuting}, title = {Abella: A~System for Reasoning about Relational Specifications}, volume = {7}, number = {2}, year = {2014}, pages = {1-89}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGMNTW-jfr14.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BCGMNTW-jfr14.pdf}, doi = {10.6092/issn.1972-5787/4650}, abstract = {The Abella interactive theorem prover is based on an intuitionistic logic that allows for inductive and co-inductive reasoning over relations. Abella supports the \(\lambda\)-tree approach to treating syntax containing binders: it~allows simply typed \(\lambda\)-terms to be used to represent such syntax and it provides higher-order (pattern) unification, the \(\nabla\) quantifier, and nominal constants for reasoning about these representations. As such, it is a suitable vehicle for formalizing the meta-theory of formal systems such as logics and programming languages. This tutorial exposes Abella incrementally, starting with its capabilities at a first-order logic level and gradually presenting more sophisticated features, ending with the support it offers to the \emph{two-level logic approach} to meta-theoretic reasoning. Along the way, we show how Abella can be used prove theorems involving natural numbers, lists, and automata, as well as involving typed and untyped \(\lambda\)-calculi and the \(\pi\)-calculus.} }

@inproceedings{BDS-csl15, address = {Berlin, Germany}, month = sep, year = 2015, volume = {41}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Kreuzer, Stephan}, acronym = {{CSL}'15}, booktitle = {{P}roceedings of the 24th {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'15)}, author = {Baelde, David and Doumane, Amina and Saurin, Alexis}, title = {Least and Greatest Fixed Points in Ludics}, pages = {549-566}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDS-csl15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDS-csl15.pdf}, doi = {10.4230/LIPIcs.CSL.2015.549}, abstract = {Various logics have been introduced in order to reason over (co)inductive specifications and, through the Curry-Howard correspondence, to study computation over inductive and coinductive data. The logic mu-MALL is one of those logics, extending multiplicative and additive linear logic with least and greatest fixed point operators.\par In this paper, we investigate the semantics of mu-MALL proofs in (computational) ludics. This framework is built around the notion of design, which can be seen as an analogue of the strategies of game semantics. The infinitary nature of designs makes them particularly well suited for representing computations over infinite data.\par We provide mu-MALL with a denotational semantics, interpreting proofs by designs and formulas by particular sets of designs called behaviours. Then we prove a completeness result for the class of {"}essentially finite designs{"}, which are those designs performing a finite computation followed by a copycat. On the way to completeness, we investigate semantic inclusion, proving its decidability (given two formulas, we can decide whether the semantics of one is included in the other's) and completeness (if semantic inclusion holds, the corresponding implication is provable in mu-MALL).} }

@inproceedings{BDH-concur15, address = {Madrid, Spain}, month = sep, year = 2015, volume = {42}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Aceto, Luca and de Frutos-Escrig, David}, acronym = {{CONCUR}'15}, booktitle = {{P}roceedings of the 26th {I}nternational {C}onference on {C}oncurrency {T}heory ({CONCUR}'15)}, author = {Baelde, David and Delaune, St{\'e}phanie and Hirschi, Lucca}, title = {Partial Order Reduction for Security Protocols}, pages = {497-510}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/BDH-concur15.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDH-concur15.pdf}, doi = {10.4230/LIPIcs.CONCUR.2015.497}, 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 (\textit{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.\par 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 elim- inate 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 \textsf{Apte}, and demonstrated that it achieves the expected speedup on various protocols.} }

@inproceedings{DBS-csl16, address = {Marseille, France}, month = sep, year = 2016, volume = {62}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Regnier, Laurent and Talbot, Jean-Marc}, acronym = {{CSL}'16}, booktitle = {{P}roceedings of the 25th {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'16)}, author = {Amina Doumane and David Baelde and Alexis Saurin}, title = {Infinitary proof theory: the multiplicative additive case}, pages = {42:1-42:17}, doi = {10.4230/LIPIcs.CSL.2016.42}, abstract = {Infinitary and regular proofs are commonly used in fixed point logics. Being natural intermediate devices between semantics and traditional finitary proof systems, they are commonly found in completeness arguments, automated deduction, verification, etc. However, their proof theory is surprisingly underdeveloped. In particular, very little is known about the computational behavior of such proofs through cut elimination. Taking such aspects into account has unlocked rich developments at the intersection of proof theory and programming language theory. One would hope that extending this to infinitary calculi would lead, e.g., to a better understanding of recursion and corecursion in programming languages. Structural proof theory is notably based on two fundamental properties of a proof system: cut elimination and focalization. The first one is only known to hold for restricted (purely additive) infinitary calculi, thanks to the work of Santocanale and Fortier; the second one has never been studied in infinitary systems. In this paper, we consider the infinitary proof system muMALLi for multiplicative and additive linear logic extended with least and greatest fixed points, and prove these two key results. We thus establish muMALLi as a satisfying computational proof system in itself, rather than just an intermediate device in the study of finitary proof systems.} }

@inproceedings{BLS-hal15, address = {Marseille, France}, month = sep, year = 2016, volume = {62}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Regnier, Laurent and Talbot, Jean-Marc}, acronym = {{CSL}'16}, booktitle = {{P}roceedings of the 25th {A}nnual {EACSL} {C}onference on {C}omputer {S}cience {L}ogic ({CSL}'16)}, author = {Baelde, David and Lunel, Simon and Schmitz, Sylvain}, title = {A~Sequent Calculus for a Modal Logic on Finite Data Trees}, pages = {32:1-32:16}, url = {https://hal.inria.fr/hal-01191172}, doi = {10.4230/LIPIcs.CSL.2016.32}, abstract = {We investigate the proof theory of a modal fragment of XPath equipped with data (in)equality tests over finite data trees, i.e. over finite unranked trees where nodes are labelled with both a symbol from a finite alphabet and a single data value from an infinite domain. We present a sound and complete sequent calculus for this logic, which yields the optimal PSPACE complexity bound for its validity problem.} }

@inproceedings{DBHS-lics16, address = {New York City, USA}, month = jul, year = 2016, publisher = {ACM Press}, editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan}, acronym = {{LICS}'16}, booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)}, author = {Amina Doumane and David Baelde and Lucca Hirschi and Alexis Saurin}, title = {Towards Completeness via Proof Search in the Linear Time {{\(\mu\)}}-calculus}, pages = {377-386}, url = {https://hal.archives-ouvertes.fr/hal-01275289/}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DBHS-lics16.pdf}, doi = {10.1145/2933575.2933598}, abstract = {Modal \(\mu\)-calculus is one of the central languages of logic and verification, whose study involves notoriously complex objects: automata over infinite structures on the model-theoretical side; infinite proofs and proofs by (co)induction on the proof-theoretical side. Nevertheless, axiomatizations have been given for both linear and branching time \(\mu\)-calculi, with quite involved completeness arguments. We come back to this central problem, considering it from a proof search viewpoint, and provide some new completeness arguments in the linear time \(\mu\)-calculus. Our results only deal with restricted classes of formulas that closely correspond to (non-alternating) \(\omega\)-automata but, compared to earlier proofs, our completeness arguments are direct and constructive. We first consider a natural circular proof system based on sequent calculus, and show that it is complete for inclusions of parity automata directly expressed as formulas, making use of Safra's construction directly in proof search. We then consider the corresponding finitary proof system, featuring (co)induction rules, and provide a partial translation result from circular to finitary proofs. This yields completeness of the finitary proof system for inclusions of sufficiently deterministic parity automata, and finally for arbitrary B{\"u}chi automata.} }

@inproceedings{HBD-sp16, address = {San Jose, California, USA}, month = may, year = 2016, publisher = {IEEECSP}, editor = {Locasto, Michael and Shmatikov, Vitaly and Erlingsson, {\'U}lfar}, acronym = {{S\&P}'16}, booktitle = {{P}roceedings of the 37th {IEEE} {S}ymposium on {S}ecurity and {P}rivacy ({S\&P}'16)}, author = {Hirschi, Lucca and Baelde, David and Delaune, St{\'e}phanie}, title = {A~method for verifying privacy-type properties: the~unbounded case}, pages = {564-581}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/HBD-sp16.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HBD-sp16.pdf}, doi = {10.1109/SP.2016.40}, abstract = {In~this paper, we~consider the problem of verifying anonymity and unlinkability in the symbolic model, where protocols are represented as processes in a variant of the applied pi calculus notably used in the Proverif tool. Existing tools and techniques do not allow one to verify directly these properties, expressed as behavioral equivalences. We propose a different approach: we design two conditions on protocols which are sufficient to ensure anonymity and unlinkability, and which can then be effectively checked automatically using Proverif. Our two conditions correspond to two broad classes of attacks on unlinkability, corresponding to data and control-flow leaks.\par This theoretical result is general enough to apply to a wide class of protocols. In particular, we apply our techniques to provide the first formal security proof of the BAC protocol (e-passport). Our work has also lead to the discovery of new attacks, including one on the LAK protocol (RFID authentication) which was previously claimed to be unlinkable (in~a weak sense) and one on the PACE protocol (e-passport).} }

@comment{{B-arxiv16, author = Bollig, Benedikt, affiliation = aff-LSVmexico, title = One-Counter Automata with Counter Visibility, institution = Computing Research Repository, number = 1602.05940, month = feb, nmonth = 2, year = 2016, type = RR, axeLSV = mexico, NOcontrat = "", url = http://arxiv.org/abs/1602.05940, PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf", lsvdate-new = 20160222, lsvdate-upd = 20160222, lsvdate-pub = 20160222, lsv-category = "rapl", wwwpublic = "public and ccsb", note = 18~pages, abstract = "In a one-counter automaton (OCA), one can read a letter from some finite alphabet, increment and decrement the counter by one, or test it for zero. It is well-known that universality and language inclusion for OCAs are undecidable. We consider here OCAs with counter visibility: Whenever the automaton produces a letter, it outputs the current counter value along with~it. Hence, its language is now a set of words over an infinite alphabet. We show that universality and inclusion for that model are in PSPACE, thus no harder than the corresponding problems for finite automata, which can actually be considered as a special case. In fact, we show that OCAs with counter visibility are effectively determinizable and closed under all boolean operations. As~a~strict generalization, we subsequently extend our model by registers. The general nonemptiness problem being undecidable, we impose a bound on the number of register comparisons and show that the corresponding nonemptiness problem is NP-complete.", }}

@misc{vip-D32, author = {Baelde, David and Delaune, St{\'e}phanie and Kremer, Steve}, title = {Decision procedures for equivalence based properties (part~{II})}, howpublished = {Deliverable VIP~3.2 (ANR-11-JS02-0006)}, month = sep, year = {2015}, note = {9~pages}, type = {Contract Report}, url = {http://www.lsv.fr/Publis/PAPERS/PDF/vip-d32.pdf}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/vip-d32.pdf} }

@article{BCMW-fi17, publisher = {{IOS} Press}, journal = {Fundamenta Informaticae}, author = {David Baelde and Arnaud Carayol and Ralph Matthes and Igor Walukiewicz}, title = {Preface: Special Issue of {Fixed Points in Computer Science} ({FICS}'13)}, volume = {150}, number = {3-4}, pages = {i-ii}, year = {2017}, url = {https://doi.org/10.3233/FI-2017-1468}, doi = {10.3233/FI-2017-1468} }

@inproceedings{BDGK-csf17, address = {Santa Barbara, California, USA}, month = aug, publisher = {{IEEE} Computer Society Press}, editor = {K{\"o}pf, Boris and Chong, Steve}, acronym = {{CSF}'17}, booktitle = {{P}roceedings of the 30th {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'17)}, author = {Baelde, David and Delaune, St{\'e}phanie and Gazeau, Ivan and Kremer, Steve}, title = {Symbolic Verification of Privacy-Type Properties for Security Protocols with {XOR}}, pages = {234-248}, year = {2017}, doi = {10.1109/CSF.2017.22}, pdf = {https://hal.inria.fr/hal-01533694/document}, url = {https://hal.inria.fr/hal-01533694}, abstract = {In symbolic verification of security protocols, process equivalences have recently been used extensively to model strong secrecy, anonymity and unlinkability properties. However, tool support for automated analysis of equivalence properties is limited compared to trace properties, e.g., modeling authentication and weak notions of secrecy. In this paper, we present a novel procedure for verifying equivalences on finite processes, i.e., without replication, for protocols that rely on various cryptographic primitives including exclusive or (xor). We have implemented our procedure in the tool AKISS, and successfully used it on several case studies that are outside the scope of existing tools, e.g., unlinkability on various RFID protocols, and resistance against guessing attacks on protocols that use xor.} }

@article{BDH-lmcs17, journal = {Logical Methods in Computer Science}, author = {Baelde, David and Delaune, St{\'e}phanie and Hirschi, Lucca}, title = {{A Reduced Semantics for Deciding Trace Equivalence}}, volume = {13}, number = {2:8}, year = {2017}, pages = {1-48}, doi = {10.23638/LMCS-13(2:8)2017}, pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BDH-lmcs17.pdf}, url = {https://lmcs.episciences.org/3703}, abstract = {Many privacy-type properties of security protocols can be modelled using trace equivalence properties in suitable process algebras. It has been shown that such properties can be decided for interesting classes of finite processes (i.e. without replication) by means of symbolic execution and constraint solving. However, this does not suffice to obtain practical tools. Current prototypes suffer from a classical combinatorial explosion problem caused by the exploration of many interleavings in the behaviour of processes. M{\"o}dersheim et al. [40] have tackled this problem for reachability properties using partial order reduction techniques. We revisit their work, generalize it and adapt it for equivalence checking. We obtain an optimisation in the form of a reduced symbolic semantics that eliminates redundant interleavings on the fly. The obtained partial order reduction technique has been integrated in a tool called Apte. We conducted complete benchmarks showing dramatic improvements.} }

@inproceedings{BDH-esorics18, address = {Barcelona, Spain}, month = sep, year = 2018, volume = {11098}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {Javier L{\'{o}}pez and Jianying Zhou and Miguel Soriano}, acronym = {{ESORICS}'18}, booktitle = {{P}roceedings of the 23rd {E}uropean {S}ymposium on {R}esearch in {C}omputer {S}ecurity ({ESORICS}'18)}, author = {David Baelde and St{\'e}phanie Delaune and Lucca Hirschi}, title = {{POR} for Security Protocol Equivalences - Beyond Action-Determinism}, pages = {385-405}, url = {https://arxiv.org/abs/1804.03650}, doi = {10.1007/978-3-319-99073-6\_19}, abstract = {Formal methods have proved effective to automatically analyse protocols. Recently, much research has focused on verifying trace equivalence on protocols, which is notably used to model interesting privacy properties such as anonymity or unlinkability. Several tools for checking trace equivalence rely on a naive and expensive exploration of all interleavings of concurrent actions, which calls for partial-order reduction (POR) techniques. In this paper, we present the first POR technique for protocol equivalences that does not rely on an action-determinism assumption: we recast trace equivalence as a reachability problem, to which persistent and sleep set techniques can be applied, and we show how to effectively apply these results in the context of symbolic execution. We report on a prototype implementation, improving the tool DeepSec.} }

@inproceedings{BLS-fsttcs18, address = {Ahmedabad, India}, month = dec, year = 2018, volume = {122}, series = {Leibniz International Proceedings in Informatics}, publisher = {Leibniz-Zentrum f{\"u}r Informatik}, editor = {Sumit Ganguly and Paritosh Pandya}, acronym = {{FSTTCS}'18}, booktitle = {{P}roceedings of the 38th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'18)}, author = {Baelde, David and Lick, Anthony and Schmitz, Sylvain}, title = {A Hypersequent Calculus with Clusters for Tense Logic over Ordinals}, pages = {15:1-15:19}, url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9914}, pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9914/pdf/LIPIcs-FSTTCS-2018-15.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2018.15}, abstract = {Prior's tense logic forms the core of linear temporal logic, with both past-and future-looking modalities. We present a sound and complete proof system for tense logic over ordinals. Technically, this is a hypersequent system, enriched with an ordering, clusters, and annotations. The system is designed with proof search algorithms in mind, and yields an optimal coNP complexity for the validity problem. It entails a small model property for tense logic over ordinals: every satisfiable formula has a model of order type at most \(\omega^2\). It also allows to answer the validity problem for ordinals below or exactly equal to a given one.} }

@inproceedings{BLS-pods19, address = {Amsterdam, Netherlands}, month = jun # {-} # jul, publisher = {ACM Press}, editor = {Christoph Koch}, acronym = {{PODS}'19}, booktitle = {{P}roceedings of the 38th {A}nnual {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'19)}, author = {Baelde, David and Lick, Anthony and Schmitz, Sylvain}, title = {Decidable {XP}ath Fragments in the Real World}, pages = {285-302}, year = 2019, doi = {10.1145/3294052.3319685}, url = {https://hal.inria.fr/hal-01852475}, abstract = {XPath is arguably the most popular query language for selecting elements in XML documents. Besides query evaluation, query satisfiability and containment are the main computational problems for XPath; they are useful, for instance, to detect dead code or validate query optimisations. These problems are undecidable in general, but several fragments have been identified over time for which satisfiability (or query containment) is decidable: CoreXPath 1.0 and 2.0 without so-called data joins, fragments with data joins but limited navigation, etc. However, these fragments are often given in a simplified syntax, and sometimes wrt. a simplified XPath semantics. Moreover, they have been studied mostly with theoretical motivations, with little consideration for the practically relevant features of XPath. To investigate the practical impact of these theoretical fragments, we design a benchmark compiling thousands of real-world XPath queries extracted from open-source projects. These queries are then matched against syntactic fragments from the literature. We investigate how to extend these fragments with seldom-considered features such as free variables, data tests, data joins, and the last() and id() functions, for which we provide both undecidability and decidability results. We analyse the coverage of the original and extended fragments, and further provide a glimpse at which other practically-motivated features might be worth investigating in the future.} }

@inproceedings{BLS-aiml18, address = {Bern, Switzerland}, month = aug, year = 2018, publisher = {College Publications}, editor = {Guram Bezhanishvili and Giovanna D'Agostino and George Metcalfe and Thomas Studer}, acronym = {{AiML}'18}, booktitle = {{P}roceedings of the 10th {C}onference on {A}dvances in {M}odal {L}ogics ({AiML}'18)}, author = {Baelde, David and Lick, Anthony and Schmitz, Sylvain}, title = {A Hypersequent Calculus with Clusters for Linear Frames}, pages = {36-55}, url = {https://hal.inria.fr/hal-01756126}, abstract = {The logic Kt4.3 is the basic modal logic of linear frames. Along with its extensions, it is found at the core of linear-time temporal logics and logics on words. In this paper, we consider the problem of designing proof systems for these logics, in such a way that proof search yields decision procedures for validity with an optimal complexity---coNP in this case. In earlier work, Indrzejczak has proposed an ordered hypersequent calculus that is sound and complete for Kt4.3 but does not yield any decision procedure. We refine his approach, using a hypersequent structure that corresponds to weak rather than strict total orders, and using annotations that reflect the model-theoretic insights given by small models for Kt4.3. We obtain a sound and complete calculus with an associated coNP proof search algorithm. These results extend naturally to the cases of unbounded and dense frames, and to the complexity of the two-variable fragment of first-order logic over total orders.} }

@article{HBD-jcs19, publisher = {{IOS} Press}, journal = {Journal of Computer Security}, author = {Hirschi, Lucca and Baelde, David and Delaune, St{\'e}phanie}, title = {A method for unbounded verification of privacy-type properties}, volume = {27}, number = {3}, pages = {277-342}, year = 2019, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/HBD-jcs19.pdf}, doi = {10.3233/JCS-171070}, url = {https://content.iospress.com/articles/journal-of-computer-security/jcs171070} }

@inproceedings{BDJKM-csl21, address = {online}, month = may, publisher = {{IEEE} Press}, editor = {Alina Oprea and Thorsten Holz}, acronym = {{S\&P}'21}, booktitle = {{P}roceedings of the 42nd IEEE Symposium on Security and Privacy ({S\&P}'21)}, author = {Baelde, David and Delaune, St{\'e}phanie and Jacomme, Charlie and Koutsos, Adrien and Moreau, Sol{\`e}ne}, title = {An {I}nteractive {P}rover for {P}rotocol {V}erification in the {C}omputational {M}odel}, year = {2021}, pdf = {https://hal.archives-ouvertes.fr/hal-03172119}, url = {https://hal.archives-ouvertes.fr/hal-03172119}, note = {To appear} }

@phdthesis{baelde-hdr2021, author = {Baelde, David}, title = {Contributions to the {V}erification of {C}ryptographic {P}rotocols}, school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France}, type = {M{\'e}moire d'habilitation}, year = 2021, month = feb, pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Baelde-Hab2021.pdf}, url = {http://www.lsv.fr/~baelde/hdr/index.html} }

@inproceedings{BDM-csf20, address = {Boston, MA, USA}, month = jul, publisher = {{IEEE} Computer Society Press}, editor = {Jia, Limin and K{\"u}sters, Ralf}, acronym = {{CSF}'19}, booktitle = {{P}roceedings of the 33rd {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'20)}, author = {David Baelde and St{\'e}phanie Delaune and Sol{\`e}ne Moreau}, title = {A Method for Proving Unlinkability of Stateful Protocols}, pages = {169--183}, year = 2020, url = {https://hal.archives-ouvertes.fr/hal-02459984/}, abstract = {The rise of contactless and wireless devices such as mobile phones and RFID chips justifies significant concerns over privacy, and calls for communication protocols that ensure some form of unlinkability. Formally specifying this property is difficult and context-dependent, and analysing it is very complex; as is common with security protocols, several incorrect unlinkability claims can be found in the literature. Formal verification is therefore desirable, but current techniques are not sufficient to directly analyse unlinkability. In [Hirschi et al., SP'19], two conditions have been identified that imply unlinkability and can be automatically verified. This work, however, only considers a restricted class of protocols. We adapt their formal definition as well as their proof method to the common setting of RFID authentication protocols, where readers access a central database of authorised users. Moreover, we also consider protocols where readers may update their database, and tags may also carry a mutable state. We propose sufficient conditions to ensure unlinkability, find new attacks, and obtain new proofs of unlinkability using Tamarin to establish our sufficient conditions.} }

@article{BFNS-mscs20, publisher = {Cambridge University Press}, journal = {Mathematical Structures in Computer Science}, author = {David Baelde and Amy P. Felty and Gopalan Nadathur and Alexis Saurin}, title = {A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller's 60th birthday}, volume = {29}, number = {8}, pages = {1007--1008}, year = 2020, doi = {10.1017/S0960129519000136}, abstract = {The genesis of this special issue was in a meeting that took place at UniversitÃ© Paris Diderot on December 15 and 16, 2016. Dale Miller, Professor at Ã‰cole polytechnique, had turned 60 a few days earlier. In a career spanning over three decades and in work conducted in collaboration with several students and colleagues, Dale had had a significant influence in an area that can be described as structural proof theory and its application to computation and reasoning. In recognition of this fact, several of his collaborators thought it appropriate to celebrate the occasion by organizing a symposium on topics broadly connected to his areas of interest and achievements. The meeting was a success in several senses: it was attended by over 35 people, there were 15 technical presentations describing new results, and, quite gratifyingly, we managed to spring the event as a complete surprise to Dale.} }

*This file was generated by
bibtex2html 1.98.*