Deciding knowledge in security protocols under equational theories, Theor. Comput. Sci, vol.367, issue.1-2, pp.2-32, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00099982
Term rewriting and all that, 1998. ,
Unification in the union of disjoint equational theories: Combining decision procedures, Journal of Symbolic Computation, vol.21, issue.2, pp.211-243, 1996. ,
Unification theory, Handbook of Automated Reasoning, pp.445-532, 2001. ,
An on-the-fly model-checker for security protocol analysis, Computer Security -ESORICS 2003, 8th European Symposium on Research in Computer Security, vol.2808, pp.253-270, 2003. ,
Modeling and verifying security protocols with the Applied Pi calculus and proverif, Foundations and Trends in Privacy and Security, vol.1, issue.1-2, pp.1-135, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01423760
On forward closure and the finite variant property, Frontiers of Combining Systems -9th International Symposium, vol.8152, pp.327-342, 2013. ,
Computing knowledge in security protocols under convergent equational theories, J. Autom. Reasoning, vol.48, issue.2, pp.219-262, 2012. ,
On ends-toends encryption: Asynchronous group messaging with strong security guarantees, Proceedings of the, 2018. ,
, ACM SIGSAC Conference on Computer and Communications Security, pp.1802-1819, 2018.
Syntacticness, cycle-syntacticness, and shallow theories, Inf. Comput, vol.111, issue.1, pp.154-191, 1994. ,
The finite variant property: How to get rid of some algebraic properties, Rewriting Techniques and Applications, vol.3467, pp.294-307, 2005. ,
Built-in variant generation and unification, and their applications in Maude 2.7, Automated Reasoning -8th International Joint Conference, IJCAR 2016, vol.9706, pp.183-192, 2016. ,
Rule-based unification in combined theories and the finite variant property, Language and Automata Theory and Applications -13th International Conference, vol.11417, pp.356-367, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-01988419
Hierarchical combination, 24 -24th International Conference on Automated Deduction, vol.7898, pp.249-266, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00878649
Unification over distributive exponentiation (sub)theories, Journal of Automata, Languages and Combinatorics (JALC), vol.16, issue.2-4, pp.109-140, 2011. ,
Notions of knowledge in combinations of theories sharing constructors, Automated Deduction -CADE 26 -26th International Conference on Automated Deduction, vol.10395, pp.60-76, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01587181
Computing knowledge in equational extensions of subterm convergent theories, Mathematical Structures in Computer Science, pp.1-27, 2020. ,
URL : https://hal.archives-ouvertes.fr/hal-02966957
Maude-NPA: Cryptographic protocol analysis modulo equational properties, Foundations of Security Analysis and Design, vol.5705, pp.1-50, 2007. ,
Folding variant narrowing and optimal variant termination, J. Log. Algebr. Program, vol.81, issue.7-8, pp.898-928, 2012. ,
Completion of a set of rules modulo a set of equations, SIAM J. Comput, vol.15, issue.4, pp.1155-1194, 1986. ,
Reviving basic narrowing modulo, Frontiers of Combining Systems -12th International Symposium, vol.11715, pp.313-329, 2019. ,
Syntactic theories and unification, Logic in Computer Science, 1990. LICS '90, Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pp.270-277, 1990. ,
Automated Deduction -CADE-18, 18th International Conference on Automated Deduction, vol.2392, pp.471-485, 2002. ,
On unification modulo onesided distributivity: Algorithms, variants and asymmetry, Logical Methods in Computer Science, vol.11, issue.2, 2015. ,
The TAMARIN prover for the symbolic analysis of security protocols, Computer Aided Verification -25th International Conference, CAV 2013, vol.8044, pp.696-701, 2013. ,
Variant-based satisfiability in initial algebras, Sci. Comput. Program, vol.154, pp.3-41, 2018. ,
Work done under the supervision of Vincent Cheval and Véronique Cortier ,
Proof transformations for equational theories, Logic in Computer Science, 1990. LICS '90, Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pp.278-288, 1990. ,
Unification in a combination of arbitrary disjoint equational theories, Journal of Symbolic Computation, vol.8, pp.51-99, 1989. ,
Unification problems with one-sided distributivity, Journal of Symbolic Computation, vol.3, issue.1, pp.183-202, 1987. ,
Unification in combinations of collapse-free regular theories, Journal of Symbolic Computation, vol.3, issue.1-2, pp.153-181, 1987. ,