@inproceedings{Cry01,
  author    = {<NAME> and <NAME>},
  title     = {Finding SHA-1 Characteristics: General Results and Applications},
  pages     = {1-20},
  url        = {http://dx.doi.org/10.1007/11935230_1},
  editor    = {<NAME> and <NAME>},
  booktitle = {ASIACRYPT},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4284},
  year      = {2006},
  isbn      = {3-540-49475-8},
  abstract  = {The most efficient collision attacks on members of the SHA family presented so far all use complex characteristics which were manually constructed by Wang et al. In this report, we describe a method to search for characteristics in an automatic way. This is particularly useful for multi-block attacks, and as a proof of concept, we give a two-block collision for 64-step SHA-1 based on a new characteristic. The highest number of steps for which a SHA-1 collision was published so far was 58. We also give a unified view on the expected work factor of a collision search and the needed degrees of freedom for the search, which facilitates optimization.},
}

@phdthesis{Cry02,
  author = {<NAME>\"{a}ffer},
  title = {Cryptanalysis of AES-Based Hash Functions},
  school = {Institute for Applied Information Processing and Communications},
  year = {2011}
}

@inproceedings{Cry03,
  author = {<NAME> and <NAME> and Schl\"{a}ffer, Martin},
  title = {Finding SHA-2 Characteristics: Searching Through a Minefield of Contradictions},
  booktitle = {Proceedings of the 17th International Conference on The Theory and Application of Cryptology and Information Security},
  series = {ASIACRYPT'11},
  year = {2011},
  isbn = {978-3-642-25384-3},
  location = {Seoul, South Korea},
  pages = {288--307},
  numpages = {20},
  url = {http://dx.doi.org/10.1007/978-3-642-25385-0_16},
  doi = {10.1007/978-3-642-25385-0_16},
  acmid = {2184043},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
  keywords = {SHA-2, collision attack, differential characteristic, generalized conditions, hash functions},
}

@incollection{Cry04,
  year = {2012},
  isbn = {978-3-642-33259-3},
  booktitle = {Computer Information Systems and Industrial Management},
  volume = {7564},
  series = {Lecture Notes in Computer Science},
  editor = {<NAME> and <NAME>},
  doi = {10.1007/978-3-642-33260-9_4},
  title = {Security Margin Evaluation of SHA-3 Contest Finalists through SAT-Based Attacks},
  url = {http://dx.doi.org/10.1007/978-3-642-33260-9_4},
  publisher = {Springer Berlin Heidelberg},
  keywords = {Cryptographic hash algorithm; SHA-3 competition; algebraic cryptanalysis; logical cryptanalysis; SATisfiability solvers},
  author = {Homsirikamol, Ekawat and Morawiecki, Paweł and Rogawski, Marcin and <NAME>},
  pages = {56-67}
}

@inproceedings{Cry05,
  author = {<NAME>},
  title = {Using Walk-SAT and Rel-SAT for cryptographic key search},
  booktitle = {In Proceedings of the International Joint Conference on Artifical Intelligence},
  year = {1999},
  pages = {290--295}
}

@inproceedings{Cry05b,
  author = {<NAME>},
  title = {Logical Cryptanalysis as a SAT Problem},
  journal = {Journal of Automated Reasoning},
  year = {2000},
  pages = {165--203}
}

@incollection{Cry06,
  year = {2009},
  isbn = {978-3-642-02776-5},
  booktitle = {Theory and Applications of Satisfiability Testing - SAT 2009},
  volume = {5584},
  series = {Lecture Notes in Computer Science},
  editor = {<NAME>},
  doi = {10.1007/978-3-642-02777-2_24},
  title = {Extending SAT Solvers to Cryptographic Problems},
  url = {http://dx.doi.org/10.1007/978-3-642-02777-2_24},
  publisher = {Springer Berlin Heidelberg},
  author = {<NAME> and <NAME> and <NAME>},
  pages = {244-257}
}

@inproceedings{Cry07,
  author = {<NAME> and <NAME> and <NAME>\"{a}ffer},
  title = {Finding SHA-2 Characteristics: Searching Through a Minefield of Contradictions},
  booktitle = {ASIACRYPT},
  year = {2011},
  editor = {<NAME> and <NAME>},
  volume = {7073},
  series = {LNCS},
  pages = {288 - 307},
  publisher = {Springer},
}

@inproceedings{Cry08,
  author = {<NAME> and <NAME> and <NAME>\"{a}ffer},
  title = {Collision Attacks on the Reduced Dual-Stream Hash Function RIPEMD-128},
  booktitle = {Fast Software Encryption},
  year = {2012},
  editor = {<NAME>},
  volume = {7549},
  series = {LNCS},
  pages = {226 - 243},
  publisher = {Springer},
}

@incollection{Cry10,
  year = {2005},
  isbn = {978-3-540-25910-7},
  booktitle = {Advances in Cryptology – EUROCRYPT 2005},
  volume = {3494},
  series = {Lecture Notes in Computer Science},
  editor = {<NAME>},
  doi = {10.1007/11426639_2},
  title = {How to Break MD5 and Other Hash Functions},
  url = {http://dx.doi.org/10.1007/11426639_2},
  publisher = {Springer Berlin Heidelberg},
  author = {<NAME> and <NAME>},
  pages = {19-35}
}

@masterthesis{Cry15,
  author = {<NAME>\"{a}ffer},
  title = {Cryptanalysis of MD4},
  year = {2006}
}

@inproceedings{Cry16,
  author = {<NAME> and <NAME> and <NAME> and <NAME> and <NAME>\"{a}ffer},
  title = {Linear Propagation in Efficient Guess-and-Determine Attacks},
  booktitle = {Preproceedings of the International Workshop on Coding and Cryptography},
  year = {2013},
  editor = {<NAME>, <NAME>, <NAME>},
  pages = {193 - 202}
}

@inproceedings{Sat01,
  title = {The complexity of theorem-proving procedures},
  author = {Cook, <NAME>},
  booktitle = {Proceedings of the third annual ACM symposium on Theory of computing},
  pages = {151--158},
  year = {1971},
  organization = {ACM}
}


@article{Sat02,
  title = {Universal sequential search problems},
  author = {<NAME>},
  journal = {Problemy Peredachi Informatsii},
  volume = {9},
  number = {3},
  pages = {115--116},
  year = {1973},
  publisher = {Russian Academy of Sciences, Branch of Informatics, Computer Equipment and Automatization}
}

@incollection{Sat03,
  year = {2005},
  isbn = {978-3-540-29051-3},
  booktitle = {Frontiers of Combining Systems},
  volume = {3717},
  series = {Lecture Notes in Computer Science},
  editor = {<NAME>},
  doi = {10.1007/11559306_11},
  title = {Logical Analysis of Hash Functions},
  url = {http://dx.doi.org/10.1007/11559306_11},
  publisher = {Springer Berlin Heidelberg},
  author = {<NAME> and <NAME>},
  pages = {200-215}
}

@article{Sat05,
  author = {<NAME> and <NAME>},
  title = {A Computing Procedure for Quantification Theory},
  journal = {J. ACM},
  issue_date = {July 1960},
  volume = {7},
  number = {3},
  month = jul,
  year = {1960},
  issn = {0004-5411},
  pages = {201--215},
  numpages = {15},
  url = {http://doi.acm.org/10.1145/321033.321034},
  doi = {10.1145/321033.321034},
  acmid = {321034},
  publisher = {ACM},
  address = {New York, NY, USA},
}

@incollection{Sat06,
  year = {2007},
  isbn = {978-3-540-74564-8},
  booktitle = {KI 2007: Advances in Artificial Intelligence},
  volume = {4667},
  series = {Lecture Notes in Computer Science},
  editor = {<NAME>},
  doi = {10.1007/978-3-540-74565-5_2},
  title = {Early History and Perspectives of Automated Deduction},
  url = {http://dx.doi.org/10.1007/978-3-540-74565-5_2},
  publisher = {Springer Berlin Heidelberg},
  author = {<NAME>},
  pages = {2-18}
}

@article{Sat07,
  title = {A deterministic $(2-2/(k+1))^n$ algorithm for $k$-SAT based on local search},
  journal = {Theoretical Computer Science},
  volume = {289},
  number = {1},
  pages = {69 - 83},
  year = {2002},
  issn = {0304-3975},
  doi = {http://dx.doi.org/10.1016/S0304-3975(01)00174-8},
  url = {http://www.sciencedirect.com/science/article/pii/S0304397501001748},
  author = {<NAME> and <NAME> and <NAME> and <NAME> and <NAME> and <NAME> and <NAME> and <NAME>}
}

@incollection{Sat08,
  year = {1999},
  isbn = {978-1-4419-4813-7},
  booktitle = {Handbook of Combinatorial Optimization},
  editor = {<NAME> and <NAME>.},
  doi = {10.1007/978-1-4757-3023-4_7},
  title = {Algorithms for the Satisfiability (SAT) Problem},
  url = {http://dx.doi.org/10.1007/978-1-4757-3023-4_7},
  publisher = {Springer US},
  author = {<NAME> <NAME>. and <NAME>.},
  pages = {379-572},
  language = {English}
}

@techreport{Sat09,
  booktitle = {DIMACS Challenge},
  howpublished = {ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc/},
  keywords = {satisfiability, standards},
  priority = {0},
  title = {{Satisfiability Suggested Format}},
  url = {ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc/},
  year = {1993}
}

@misc{Sat10,
  author = {<NAME>},
  title = {Construction of Differential Characteristics in ARX Designs -- Application to Skein},
  howpublished = {Cryptology ePrint Archive, Report 2012/668},
  year = {2012},
  note = {\url{http://eprint.iacr.org/}},
}

@article{Sat11,
  title = {Towards Finding Optimal Differential Characteristics for ARX: Application to Salsa20},
  author = {<NAME> and <NAME>},
  year = {2013},
  note = {\url{http://eprint.iacr.org/}},
}

@book{Sat20,
  author = {<NAME>. and <NAME>. and <NAME> <NAME>.},
  title = {Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications},
  year = {2009},
  isbn = {1586039296, 9781586039295},
  publisher = {IOS Press},
  address = {Amsterdam, The Netherlands, The Netherlands}
}

@online{Sat21,
  author = {SATlive},
  title = {The international SAT Competitions web page},
  year = 2013,
  url = {http://satcompetition.org/},
  urldate = {2014-02-27}
}

@incollection{Sat22,
  year = {2013},
  isbn = {978-3-642-39070-8},
  booktitle = {Theory and Applications of Satisfiability Testing – SAT 2013},
  volume = {7962},
  series = {Lecture Notes in Computer Science},
  editor = {<NAME> <NAME>},
  doi = {10.1007/978-3-642-39071-5_3},
  title = {There Are No CNF Problems},
  url = {http://dx.doi.org/10.1007/978-3-642-39071-5_3},
  publisher = {Springer Berlin Heidelberg},
  author = {<NAME>.},
  pages = {19-21}
}

@inproceedings{Sat30,
  title = {A single-instance incremental SAT formulation of proof-and counterexample-based abstraction},
  author = {<NAME> and <NAME> <NAME>},
  url = {http://arxiv.org/pdf/1008.2021.pdf},
  booktitle = {Formal Methods in Computer-Aided Design (FMCAD), 2010},
  pages = {181--188},
  year = {2010},
  organization = {IEEE}
}

