arXiv subjects

Vincent Cheval

Publications and source records attributed to Vincent Cheval.

8 recordsLinked to original sources

arXiv2025

On the Complexity of the Optimal Correlated Equilibria in Extensive-Form Games

A major open question in algorithmic game theory is whether normal-form correlated equilibria (NFCE) can be computed efficiently in succinct games such as extensive-form games. Motivated by this question, we study the associated Threshold problem: deciding whether there exists a correlated equilibrium whose value exceeds a given threshold. We prove that this problem is PSPACE-hard for NFCE in multiplayer extensive-form games with perfect recall, even for fixed thresholds. To contextualize this result, we also establish the complexity of the Threshold problem for Nash equilibria in this setting, showing it is ER-complete. These results uncover a surprising complexity reversal: while optimal correlated equilibria are computationally simpler than optimal Nash in normal-form games, the opposite holds in extensive-form games, where computing optimal correlated equilibria is strictly harder unless ER is equal to PSPACE. We also address a related question by von Stengel and Forges, who introduced the notions of extensive-form correlated equilibrium (EFCE) and agent-form correlated equilibrium (AFCE). They asked how difficult the Threshold problem is for AFCE; we answer this question by proving that it is NP-hard, even in two-player games without chance nodes. Complementing our hardness results, we establish tight complexity classifications for the Threshold problem across several correlated equilibrium concepts - including EFCE, AFCE, normal-form coarse, extensive-form coarse, and agent-form coarse correlated equilibria. For each of these solution concepts in multiplayer stochastic extensive-form games with perfect recall, we prove NP-completeness by providing matching NP upper bounds to the previously known hardness results. Finally, we also place the problem of computing arbitrary Nash Equilibria in extensive-form games in FixP, matching its complexity in normal-form games.

cs.GT↗

arXiv2024

Automatic verification of Finite Variant Property beyond convergent equational theories

Computer-aided analysis of security protocols heavily relies on equational theories to model cryptographic primitives. Most automated verifiers for security protocols focus on equational theories that satisfy the Finite Variant Property (FVP), for which solving unification is decidable. However, they either require to prove FVP by hand or at least to provide a representation as an E-convergent rewrite system, usually E being at most the equational theory for an associative and commutative function symbol (AC). The verifier ProVerif is probably the only exception amongst these tools as it automatically proves FVP without requiring a representation, but on a small class of equational theories. In this work, we propose a novel semi-decision procedure for proving FVP, without the need for a specific representation, and for a class of theories that goes beyond the ones expressed by an E-convergent rewrite system. We implemented a prototype and successfully applied it on several theories from the literature.

cs.CR↗

arXiv2024

Differential Tree Automata

A rationally dynamically algebraic (RDA) power series is one that arises as (a component of) the solution of a system of differential equations of the form $\boldsymbol{y}' = F(\boldsymbol{y})$, where $F$ is a vector of rational functions that is defined at $\boldsymbol{y}(0)$. RDA power series subsume algebraic power series and are a proper subclass of differentially algebraic power series (those that satisfy a univariate polynomial-differential equation). We give a combinatorial characterisation of RDA power series in terms of exponential generating functions of regular languages of labelled trees. Motivated by this connection, we define the notion of a differential tree automaton. Differential tree automata generalise weighted tree automata by allowing the transition weights to be rational functions of the tree size. Our main result is that the ordinary generating functions of the formal tree series recognised by differential tree automata are exactly the differentially algebraic power series. The proof of this result establishes a general form of recurrence satisfied by the sequence of coefficients of a differentially algebraic power series, generalising Reutenauer's matrix representation of polynomially recursive sequences. As a corollary we obtain a procedure for determining equality of differential tree automata.

cs.FL↗

arXiv2023

On Learning Polynomial Recursive Programs

We introduce the class of P-finite automata. These are a generalisation of weighted automata, in which the weights of transitions can depend polynomially on the length of the input word. P-finite automata can also be viewed as simple tail-recursive programs in which the arguments of recursive calls can non-linearly refer to a variable that counts the number of recursive calls. The nomenclature is motivated by the fact that over a unary alphabet P-finite automata compute so-called P-finite sequences, that is, sequences that satisfy a linear recurrence with polynomial coefficients. Our main result shows that P-finite automata can be learned in polynomial time in Angluin's MAT exact learning model. This generalises the classical results that deterministic finite automata and weighted automata over a field are respectively polynomial-time learnable in the MAT model.

cs.LO↗

arXiv2023

Automatic verification of transparency protocols (extended version)

Transparency protocols are protocols whose actions can be publicly monitored by observers (such observers may include regulators, rights advocacy groups, or the general public). The observed actions are typically usages of private keys such as decryptions, and signings. Examples of transparency protocols include certificate transparency, cryptocurrency, transparent decryption, and electronic voting. These protocols usually pose a challenge for automatic verification, because they involve sophisticated data types that have strong properties, such as Merkle trees, that allow compact proofs of data presence and tree extension. We address this challenge by introducing new features in ProVerif, and a methodology for using them. With our methodology, it is possible to describe the data type quite abstractly, using ProVerif axioms, and prove the correctness of the protocol using those axioms as assumptions. Then, in separate steps, one can define one or more concrete implementations of the data type, and again use ProVerif to show that the implementations satisfy the assumptions that were coded as axioms. This helps make compositional proofs, splitting the proof burden into several manageable pieces. We illustrate the methodology and features by providing the first formal verification of the transparent decryption and certificate transparency protocols with a precise modelling of the Merkle tree data structure.

cs.CR↗

arXiv2022

DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice

Automated verification has become an essential part in the security evaluation of cryptographic protocols. In this context privacy-type properties are often modelled by indistinguishability statements, expressed as behavioural equivalences in a process calculus. In this paper we contribute both to the theory and practice of this verification problem. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity and provide a decision procedure for these equivalences in the case of a bounded number of protocol sessions. Our procedure is the first to decide trace equivalence and labelled bisimilarity exactly for a large variety of cryptographic primitives -- those that can be represented by a subterm convergent destructor rewrite system. We also implemented the procedure in a new tool, DeepSec. We showed through extensive experiments that it is significantly more efficient than other similar tools, while at the same time raises the scope of the protocols that can be analysed.

cs.CR↗

arXiv2014

DTKI: a new formalized PKI with no trusted parties

The security of public key validation protocols for web-based applications has recently attracted attention because of weaknesses in the certificate authority model, and consequent attacks. Recent proposals using public logs have succeeded in making certificate management more transparent and verifiable. However, those proposals involve a fixed set of authorities. This means an oligopoly is created. Another problem with current log-based system is their heavy reliance on trusted parties that monitor the logs. We propose a distributed transparent key infrastructure (DTKI), which greatly reduces the oligopoly of service providers and allows verification of the behaviour of trusted parties. In addition, this paper formalises the public log data structure and provides a formal analysis of the security that DTKI guarantees.

cs.CR↗

arXiv2014

Composing security protocols: from confidentiality to privacy

Security protocols are used in many of our daily-life applications, and our privacy largely depends on their design. Formal verification techniques have proved their usefulness to analyse these protocols, but they become so complex that modular techniques have to be developed. We propose several results to safely compose security protocols. We consider arbitrary primitives modeled using an equational theory, and a rich process algebra close to the applied pi calculus. Relying on these composition results, we are able to derive some security properties on a protocol from the security analysis performed on each sub-protocol individually. We consider parallel composition and the case of key-exchange protocols. Our results apply to deal with confidentiality but also privacy-type properties (e.g. anonymity, unlinkability) expressed using a notion of equivalence. We illustrate the usefulness of our composition results on protocols from the 3G phone application and electronic passport.

cs.CR↗