S. Goldwasser and S. Micali, Probabilistic encryption, J. Comput. Syst. Sci, vol.28, issue.2, pp.270-299, 1984.

V. Shoup, Sequences of games: a tool for taming complexity in security proofs, Cryptology ePrint Archive, 2004.

M. Bellare and P. Rogaway, The security of triple encryption and a framework for code-based game-playing proofs, Advances in Cryptology -EUROCRYPT 2006, ser, vol.4004, pp.409-426, 2006.

S. Halevi, A plausible approach to computer-aided cryptographic proofs, Cryptology ePrint Archive, 2005.

B. Blanchet, A computationally sound mechanized prover for security protocols, 27th IEEE Symposium on Security and Privacy, pp.140-154, 2006.

G. Barthe, B. Grégoire, and S. Zanella-béguelin, Formal certification of code-based cryptographic proofs, 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.90-101, 2009.

G. Barthe, B. Grégoire, S. Heraud, and S. Zanella-béguelin, Computer-aided security proofs for the working cryptographer, Advances in Cryptology -CRYPTO 2011, vol.6841, pp.71-90, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01112075

G. Barthe, J. M. Crespo, B. Grégoire, C. Kunz, Y. Lakhnech et al., Fully automated analysis of padding-based encryption in the computational model, 2013 ACM SIGSAC Conference on Computer and Communications Security, CCS'13, pp.1247-1260, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00935737

G. Barthe, B. Grégoire, and B. Schmidt, Automated proofs of pairing-based cryptography, Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, pp.1156-1168, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01246713

G. Barthe, X. Fan, J. Gancher, B. Grégoire, C. Jacomme et al., Symbolic proofs for lattice-based cryptography, Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pp.538-555, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01959391

G. Barthe, S. Belaïd, F. Dupressoir, P. Fouque, B. Grégoire et al., Verified proofs of higher-order masking, Advances in Cryptology -EUROCRYPT 2015 -34th Annual International Conference on the Theory and Applications of Cryptographic Techniques, vol.9056, pp.457-485, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01216699

T. Nipkow, Unification in primal algebras, their powers and their varieties, J. ACM, vol.37, issue.4, pp.742-776, 1990.

, Solveq github repository

, Easycyrpt github repository

, Maskverif source files

J. K. Millen and V. Shmatikov, Constraint solving for boundedprocess cryptographic protocol analysis, CCS 2001, Proc. 8th ACM Conference on Computer and Communications Security (CCS'01), pp.166-175, 2001.

K. Knight, Unification: A multidisciplinary survey, ACM Comput. Surv, vol.21, issue.1, pp.93-124, 1989.

M. Abadi and C. Fournet, Mobile values, new names, and secure communication, 28th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp.104-115, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01423924

M. Abadi and V. Cortier, 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-00071420

G. Barthe, M. Daubignard, B. Kapron, Y. Lakhnech, and V. Laporte, On the Equality of Probabilistic Terms," in Logic for Programming, Artificial Intelligence, and Reasoning, ser. Lecture Notes in Computer, pp.46-63, 2010.

Q. Guo, P. Narendran, and D. Wolfram, Complexity of nilpotent unification and matching problems, Information and Computation, vol.162, issue.1, pp.3-23, 2000.

S. Delaune, S. Kremer, and D. Pasaila, Security protocols, constraint systems, and group theories, Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR'12), ser. Lecture Notes in Artificial Intelligence, vol.7364, pp.164-178, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00729091

M. Arnaud, V. Cortier, and S. Delaune, Combining algorithms for deciding knowledge in security protocols, Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS'07), ser. Lecture Notes in Artificial Intelligence, F. Wolter, vol.4720, pp.103-117, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00181609

S. Delaune, Easy intruder deduction problems with homomorphisms, Information Processing Letters, vol.97, issue.6, pp.213-218, 2006.

G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt et al., Easycrypt: A tutorial, Foundations of Security Analysis and Design VII -FOSAD 2012/2013 Tutorial Lectures, ser. Lecture Notes in Computer Science, vol.8604, pp.146-166, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01114366

G. Cassiers and F. Standaert, Improved bitslice masking: from optimized non-interference to probe isolation, IACR Cryptology ePrint Archive, vol.2018, p.438, 2018.

H. Groß, S. Mangard, and T. Korak, An efficient side-channel protected AES implementation with arbitrary protection order, Topics in Cryptology -CT-RSA 2017 -The Cryptographers' Track at the RSA Conference, vol.10159, pp.95-112, 2017.

M. Abadi and P. Rogaway, Reconciling two views of cryptography (The computational soundness of formal encryption), J. Cryptology, vol.15, issue.2, pp.103-127, 2002.

V. Cortier, S. Kremer, and B. Warinschi, A survey of symbolic methods in computational analysis of cryptographic systems, J. Autom. Reasoning, pp.1-35, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00379776

G. Barthe, M. Daubignard, B. M. Kapron, Y. Lakhnech, and V. Laporte, Revised Selected Papers, ser. Lecture Notes in Computer Science, Logic for Programming, Artificial Intelligence, and Reasoning -16th International Conference, LPAR-16, vol.6355, pp.46-63, 2010.

C. S. Jutla and A. Roy, A completeness theorem for pseudo-linear functions with applications to uc security, Electronic Colloquium on Computational Complexity (ECCC), vol.17, p.92, 2010.

G. Barthe, S. Belaïd, F. Dupressoir, P. Fouque, B. Grégoire et al., Strong non-interference and type-directed higherorder masking, Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp.116-129, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01410216

G. L. Mullen and D. Panario, Handbook of finite fields, 2013.

T. Avanesov, Y. Chevalier, M. Rusinowitch, and M. Turuani, Satisfiability of general intruder constraints with and without a set constructor, Journal of Symbolic Computation, vol.80, pp.27-61, 2017.
URL : https://hal.archives-ouvertes.fr/inria-00480632

R. Chang, J. Kadin, and P. Rohatgi, On unique satisfiability and the threshold behavior of randomized reductions, Journal of Computer and System Sciences, vol.50, issue.3, pp.359-373, 1995.

S. Fenner, F. Green, S. Homer, and R. Pruim, Determining acceptance possibility for a quantum computation is hard for the polynomial hierarchy, Proceedings of The Royal Society A Mathematical Physical and Engineering Sciences, vol.455, p.1999

S. Toda and M. Ogiwara, Counting classes are at least as hard as the polynomial-time hierarchy, Proceedings of the Sixth Annual Structure in Complexity Theory Conference, pp.2-12, 1991.

M. N. Vyalyi, ECC-CTR: Electronic Colloquium on Computational Complexity, technical reports, 2003.

H. Kirchner and C. Ringeissen, Combining symbolic constraint solvers on algebraic domains, J. Symb. Comput, vol.18, issue.2, pp.113-155, 1994.

Y. Chevalier and M. Rusinowitch, Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures, Theoretical Computer Science, vol.411, issue.10, pp.1261-1282, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00455290

N. , Recognizing permutation functions in polynomial time, ECCC, TR05-008, vol.173, pp.185-311, 2005.

H. Niederreiter, Orthogonal systems of polynomials in finite fields, Proceedings of the American Mathematical Society, vol.28, issue.2, pp.415-422, 1971.

D. Bogdanov, M. Niitsoo, T. Toft, and J. Willemson, Highperformance secure multi-party computation for data mining applications, International Journal of Information Security, vol.11, issue.6, pp.403-418, 2012.