B. Schneier, The Skein Hash Function Family

D. J. Bernstein, Second preimages for 6 (7? (8??)) rounds of Keccak? NIST mailing list, 2010.

A. Biryukov, O. Dunkelman, N. Keller, D. Khovratovich, and A. Shamir, Key Recovery Attacks of Practical Complexity on AES-256 Variants with up to 10 Rounds, Cryptology ePrint Archive Report, vol.374, p.374, 2009.
DOI : 10.1007/978-3-642-13190-5_15

S. A. Cook, The complexity of theorem-proving procedures, Proceedings of the third annual ACM symposium on Theory of computing , STOC '71, 1971.
DOI : 10.1145/800157.805047

S. A. Cook and D. G. Mitchell, Finding hard instances of the satisfiability problem: A survey, pp.1-17, 1997.
DOI : 10.1090/dimacs/035/01

N. Courtois and J. Pieprzyk, Cryptanalysis of Block Ciphers with Overdefined Systems of Equations, Advances in Cryptology ASIACRYPT 2002, pp.267-287, 2002.
DOI : 10.1007/3-540-36178-2_17

M. Davis, G. Logemann, and D. Loveland, A machine program for theorem-proving, Communications of the ACM, vol.7, issue.5, pp.394-397, 1962.
DOI : 10.1145/368273.368557

M. Davis and H. Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM, vol.7, issue.3, pp.201-215, 1960.
DOI : 10.1145/321033.321034

C. Fiorini, E. Martinelli, and F. Massacci, How to fake an RSA signature by encoding modular root finding as a SAT problem, Discrete Applied Mathematics, vol.130, issue.2, pp.101-127, 2003.
DOI : 10.1016/S0166-218X(02)00400-6
URL : http://doi.org/10.1016/s0166-218x(02)00400-6

G. Bertoni, Keccak sponge function family main document

K. Gaj and P. Chodowiec, FPGA and ASIC Implementatios of AES, Cryptographic Engineering, pp.235-294, 2009.
DOI : 10.1007/978-0-387-71817-0_10

J. P. Aumasson, SHA-3 proposal BLAKE

D. Jovanovic and P. Janicic, Logical Analysis of Hash Functions, Frontiers of Combining Systems, pp.200-215, 2005.
DOI : 10.1007/11559306_11

P. K. Lala, Principles of modern digital design, 2007.
DOI : 10.1002/0470125217

F. Massacci, Using Walk-SAT and Rel-SAT for cryptographic key search, Proceedings of the International Joint Conference on Artificial Intelligence, pp.290-295, 1999.

F. Mendel and S. Thomsen, An Observation on JH-512, Available online, 2008.

I. Mironov and L. Zhang, Applications of SAT Solvers to Cryptanalysis of Hash Functions, Theory and Applications of Satisfiability Testing -SAT 2006, pp.102-115, 2006.
DOI : 10.1007/11814948_13

P. Gauravaram, Grøstl ? a SHA-3 candidate, http://www.groestl.info 22. R. Rivest et al.: The MD6 hash function

M. Schlaffer, Updated Differential Analysis of Groestl Grstl website, 2011.

M. Soos, CryptoMiniSat 2.5.0, SAT Race competitive event booklet, 2010.

M. Soos, Grain of Salt ? An Automated Way to Test Stream Ciphers through SAT Solvers, Cryptanalysis, 2010.
URL : https://hal.archives-ouvertes.fr/hal-01288922

M. Soos, K. Nohl, and C. Castelluccia, Extending SAT Solvers to Cryptographic Problems, pp.244-257, 2009.
DOI : 10.1007/s10817-007-9074-1
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.157.4807

X. Wang, Y. L. Yin, and H. Yu, Finding Collisions in the Full SHA-1, Crypto. LNCS, pp.17-36, 2005.
DOI : 10.1007/11535218_2

H. Wu, Appendix For the reader's convenience, we provide an example SystemVerilog code for SHA-1 used in the experiments with our toolkit In many cases a code strongly resembles a pseudocode defining a given cryptographic algorithm. A reader familiar with C or Java should have no trouble adjusting the code to our toolkit's needs. module sha1(IN, OUT); input [511:0] IN; // input here means 512-bit message block output