{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:04:42Z","timestamp":1779087882500,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642027765","type":"print"},{"value":"9783642027772","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02777-2_24","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T06:58:18Z","timestamp":1245999498000},"page":"244-257","source":"Crossref","is-referenced-by-count":253,"title":["Extending SAT Solvers to Cryptographic Problems"],"prefix":"10.1007","author":[{"given":"Mate","family":"Soos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karsten","family":"Nohl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claude","family":"Castelluccia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Bard, G.V.: Algorithms for the solution of polynomial and linear systems of equations over finite fields, with an application to the cryptanalysis of KeeLoq. Technical report, University of Maryland Dissertation (April 2008)","DOI":"10.1007\/978-0-387-88757-9_12"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-88313-5_7","volume-title":"Computer Security - ESORICS 2008","author":"F.D. Garcia","year":"2008","unstructured":"Garcia, F.D., et al.: Dismantling MIFARE Classic. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol.\u00a05283, pp. 97\u2013114. Springer, Heidelberg (2008)"},{"key":"24_CR3","unstructured":"Nohl, K.: Description of HiTag2 (Webpage), http:\/\/cryptolib.com\/ciphers\/hitag2\/"},{"key":"24_CR4","unstructured":"Raddum, H.: Cryptanalytic results on Trivium. Technical Report 2006\/039, ECRYPT Stream Cipher Project (2006)"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/11836810_13","volume-title":"Information Security","author":"C. Canni\u00e8re De","year":"2006","unstructured":"De Canni\u00e8re, C.: Trivium: A stream cipher construction inspired by block cipher design principles. In: Katsikas, S.K., L\u00f3pez, J., Backes, M., Gritzalis, S., Preneel, B. (eds.) ISC 2006. LNCS, vol.\u00a04176, pp. 171\u2013186. Springer, Heidelberg (2006)"},{"key":"24_CR6","unstructured":"McDonald, C., Charnes, C., Pieprzyk, J.: Attacking Bivium with Minisat. Technical Report 2007\/040, ECRYPT Stream Cipher Project (2007)"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. In: Proc. of Intl. Workshop on Bounded Model Checking. ENTCS, vol.\u00a089 (2003)","DOI":"10.1016\/S1571-0661(05)82542-3"},{"issue":"3","key":"24_CR8","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"24_CR9","unstructured":"Marques, J.P., Karem, S., Sakallah, A.: Conflict analysis in search algorithms for propositional satisfiability. In: Proc. of the IEEE Intl. Conf. on Tools with Artificial Intelligence (1996)"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Malik, S., Zhao, Y., Madigan, C.F., Zhang, L., Moskewicz, M.W.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conference, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"24_CR12","first-page":"75","volume-title":"ISSAC 2002","author":"J.C. Faug\u00e8re","year":"2002","unstructured":"Faug\u00e8re, J.C.: A new efficient algorithm for computing Gr\u00f6bner bases without reduction to zero (F5). In: ISSAC 2002, pp. 75\u201383. ACM Press, New York (2002)"},{"key":"24_CR13","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1023\/A:1006326723002","volume":"24","author":"F. Massacci","year":"2000","unstructured":"Massacci, F., Marraro, L.: Logical cryptanalysis as a SAT-problem: Encoding and analysis. Journal of Automated Reasoning\u00a024, 165\u2013203 (2000)","journal-title":"Journal of Automated Reasoning"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-540-45146-4_11","volume-title":"Advances in Cryptology - CRYPTO 2003","author":"N.T. Courtois","year":"2003","unstructured":"Courtois, N.T.: Fast algebraic attacks on stream ciphers with linear feedback. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol.\u00a02729, pp. 176\u2013194. Springer, Heidelberg (2003)"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Li, C.M.: Equivalency reasoning to solve a class of hard SAT problems. Information Processing Letters 75(1-2), 75\u201381 (1999)","DOI":"10.1016\/S0020-0190(00)00126-5"},{"issue":"2","key":"24_CR16","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-007-9074-1","volume":"39","author":"C. Sinz","year":"2007","unstructured":"Sinz, C.: Visualizing SAT instances and runs of the DPLL algorithm. J. Autom. Reason.\u00a039(2), 219\u2013243 (2007)","journal-title":"J. Autom. Reason."},{"key":"24_CR17","unstructured":"Courtois, N.T., Nohl, K., O\u2019Neil, S.: Algebraic attacks on the Crypto-1 stream cipher in Mifare Classic and Oyster cards. Technical Report 2008\/166, Cryptology ePrint Archive (2008)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02777-2_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T11:12:37Z","timestamp":1739185957000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02777-2_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027765","9783642027772"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02777-2_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}