14 citations · 34 across the 11 of their papers we have counts for
12 papers
Bouncing threads for infinitary and circular proofs
David Baelde, Amina Doumane, Denis Kuperberg +1
We generalize the validity criterion for the infinitary proof system of the multiplicative additive linear logic with fixed points. Our criterion is designed to take into account a…
POR for Security Protocol Equivalences: Beyond Action-Determinism
David Baelde, Stéphanie Delaune, Lucca Hirschi
Formal methods have proved effective to automatically analyze protocols. Over the past years, much research has focused on verifying trace equivalence on protocols, which is notabl…
A method for unbounded verification of privacy-type properties
Lucca Hirschi, David Baelde, Stéphanie Delaune
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 c…
A Reduced Semantics for Deciding Trace Equivalence
David Baelde, Stéphanie Delaune, Lucca Hirschi
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 de…
Partial Order Reduction for Security Protocols
David Baelde, Stéphanie Delaune, Lucca Hirschi
Security protocols are concurrent processes that communicate using cryptography with the aim of achieving various security properties. Recent work on their formal verification has…
A reduced semantics for deciding trace equivalence using constraint systems
David Baelde, Stéphanie Delaune, Lucca Hirschi
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 de…