{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T01:07:03Z","timestamp":1767143223660,"version":"build-2238731810"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2020,5,1]],"date-time":"2020-05-01T00:00:00Z","timestamp":1588291200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2020,5,1]],"date-time":"2020-05-01T00:00:00Z","timestamp":1588291200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["SN COMPUT. SCI."],"published-print":{"date-parts":[[2020,5]]},"DOI":"10.1007\/s42979-020-00181-4","type":"journal-article","created":{"date-parts":[[2020,5,19]],"date-time":"2020-05-19T09:20:53Z","timestamp":1589880053000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["SMT Solver-Based Cryptanalysis of Block Ciphers"],"prefix":"10.1007","volume":"1","author":[{"given":"Harish Kumar","family":"Sahu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"N. Rajesh","family":"Pillai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2801-0254","authenticated-orcid":false,"given":"Indivar","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R. K.","family":"Sharma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,5,14]]},"reference":[{"key":"181_CR1","doi-asserted-by":"crossref","unstructured":"Lai X, Massey JL. A proposal for a new block encryption standard. In: Damg\u00e5rd IB, editor. Workshop on the Theory and Application of Cryptographic Techniques, Springer, 1990; pp. 389\u2013404.","DOI":"10.1007\/3-540-46877-3_35"},{"key":"181_CR2","doi-asserted-by":"crossref","unstructured":"Heinrich C. Pretty good privacy (PGP). In: Tilborg H, Jajodia S, editors. Encyclopedia of cryptography and security. Springer, 2011; pp. 955\u2013958.","DOI":"10.1007\/978-1-4419-5906-5_215"},{"key":"181_CR3","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura L, Bj\u00f8rner N. Z3: an efficient SMT solver. In: Ramakrishnan CR, Rehof J, editors. International conference on tools and algorithms for the construction and analysis of systems. Springer. 2008; pp. 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"181_CR4","doi-asserted-by":"crossref","unstructured":"Brummayer R., Biere A. Boolector: an efficient SMT solver for bit-vectors and arrays. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, 2009; pp. 174\u2013177.","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"181_CR5","unstructured":"Dutertre B., De Moura L.. The yices SMT solver. Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf, 2006; 2(2):1\u20132."},{"key":"181_CR6","doi-asserted-by":"crossref","unstructured":"Florian C, Gereon K, Sebastian J, Stefan S, Erika \u00c1. SMT-rat: an open source C++ toolbox for strategic and parallel SMT solving. In: International conference on theory and applications of satisfiability testing, pp. 360\u2013368. Springer, 2015.","DOI":"10.1007\/978-3-319-24318-4_26"},{"issue":"9","key":"181_CR7","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L De Moura","year":"2011","unstructured":"De Moura L, Bj\u00f8rner N. Satisfiability modulo theories: introduction and applications. Commun ACM. 2011;54(9):69\u201377.","journal-title":"Commun ACM"},{"key":"181_CR8","first-page":"9","volume":"12","author":"J Vanegue","year":"2012","unstructured":"Vanegue J, Heelan S, Rolles R. SMT solvers in software security. WOOT. 2012;12:9\u201322.","journal-title":"WOOT"},{"issue":"6","key":"181_CR9","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/MSP.2016.125","volume":"14","author":"A Tomb","year":"2016","unstructured":"Tomb A. Automated verification of real-world cryptographic implementations. IEEE Secur Privacy. 2016;14(6):26\u201333.","journal-title":"IEEE Secur Privacy."},{"key":"181_CR10","unstructured":"Bond B, Hawblitzel C, Kapritsos M, Leino KRM, Lorch JR, Parno B, Rane A, Setty S, Thompson L. Vale: verifying high-performance cryptographic assembly code. In: 26th USENIX security symposium (USENIX security 17). 2017; pp. 917\u2013934."},{"key":"181_CR11","doi-asserted-by":"crossref","unstructured":"Meier W. On the security of the idea block cipher. In: Workshop on the theory and application of cryptographic techniques. Springer, 1993; pp. 371\u2013385.","DOI":"10.1007\/3-540-48285-7_32"},{"key":"181_CR12","volume-title":"Differential cryptanalysis of the data encryption standard","author":"E Biham","year":"2012","unstructured":"Biham E, Shamir A. Differential cryptanalysis of the data encryption standard. Berlin: Springer; 2012."},{"key":"181_CR13","doi-asserted-by":"crossref","unstructured":"Borst J, Knudsen LR, Rijmen V. Two attacks on reduced idea. In: International conference on the theory and applications of cryptographic techniques. Springer, 1997; pp. 1\u201313.","DOI":"10.1007\/3-540-69053-0_1"},{"key":"181_CR14","doi-asserted-by":"crossref","unstructured":"Khovratovich D, Leurent G, Rechberger C. Narrow-bicliques: cryptanalysis of full idea. In: EUROCRYPT, volume 7237, Springer, 2012; pp. 392\u2013410.","DOI":"10.1007\/978-3-642-29011-4_24"},{"key":"181_CR15","doi-asserted-by":"crossref","unstructured":"K\u00f6lbl S, Leander G, Tiessen T. Observations on the Simon block cipher family. In: Annual cryptology conference. Springer, 2015; pp. 161\u2013185.","DOI":"10.1007\/978-3-662-47989-6_8"},{"key":"181_CR16","doi-asserted-by":"crossref","unstructured":"Beaulieu R, Treatman-Clark S, Shors D, Weeks B, Smith J, Wingers L. The Simon and speck lightweight block ciphers. In: Design automation conference (DAC), 2015 52nd ACM\/EDAC\/IEEE; 2015, pp. 1\u20136. IEEE.","DOI":"10.1145\/2744769.2747946"},{"key":"181_CR17","volume-title":"Experimenting with shuffle block cipher and SMT solvers","author":"M Stanek","year":"2014","unstructured":"Stanek M. Experimenting with shuffle block cipher and SMT solvers. Lyon: IACR; 2014."},{"key":"181_CR18","unstructured":"Barrett C, Stump A, Tinelli C, et\u00a0al. The SMT-lib standard: version 2.0. In: Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, England), volume\u00a013, p.\u00a014, 2010."},{"key":"181_CR19","unstructured":"Christian R. PBoolector: a parallel SMT solver for QF\\_BV by combining bit-blasting with look-ahead. Ph.D. thesis, Master\u2019s thesis, Johannes Kepler Univesit\u00e4t Linz, Linz, Austria, 2014."},{"key":"181_CR20","first-page":"53","volume":"9","author":"A Niemetz","year":"2015","unstructured":"Niemetz A, Preiner M, Biere A. Boolector 2.0. J Satisf Boolean Model Comput. 2015;9:53\u20138.","journal-title":"J Satisf Boolean Model Comput"},{"key":"181_CR21","unstructured":"Boolector at the SMT competition 2016. Technical report, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria, 2016."},{"key":"181_CR22","unstructured":"Robert B, Armin B, Florian L. Btor: bit-precise modelling of word-level problems for model checking. In: Proceedings of the joint workshops of the 6th international workshop on satisfiability modulo theories and 1st international workshop on bit-precise reasoning, pp. 33\u201338. ACM, 2008."},{"key":"181_CR23","unstructured":"John R. Tutorial: Automated formal methods with PVS, SAL, and Yices. In: Fourth IEEE international conference on software engineering and formal methods (SEFM\u201906), pp. 262\u2013262. IEEE, 2006."},{"key":"181_CR24","doi-asserted-by":"crossref","unstructured":"Alex B, Jorge N\u00a0Jr, Bart P, Joos V. New weak-key classes of idea. In: International conference on information and communications security, pp. 315\u2013326. Springer, 2002.","DOI":"10.1007\/3-540-36159-6_27"},{"key":"181_CR25","doi-asserted-by":"crossref","unstructured":"H\u00fcseyin D, Ali\u00a0Aydin S, Erkan T. A new meet-in-the-middle attack on the idea block cipher. In: International workshop on selected areas in cryptography, 2003; pp 117\u2013129. Springer.","DOI":"10.1007\/978-3-540-24654-1_9"},{"key":"181_CR26","doi-asserted-by":"crossref","unstructured":"Eli B, Orr D, Nathan K. A new attack on 6-round idea. In: International workshop on fast software encryption, 2007; pp 211\u2013224. Springer.","DOI":"10.1007\/978-3-540-74619-5_14"},{"key":"181_CR27","doi-asserted-by":"crossref","unstructured":"H\u00fcseyin D. Square-like attacks on reduced rounds of idea. In: International workshop on selected areas in cryptography, 2002; pp. 147\u2013159. Springer.","DOI":"10.1007\/3-540-36492-7_11"},{"key":"181_CR28","doi-asserted-by":"crossref","unstructured":"Eli B, Alex B, Adi S. Miss in the middle attacks on idea and khufu. In: International workshop on fast software encryption, 1999; pp. 124\u2013138. Springer.","DOI":"10.1007\/3-540-48519-8_10"},{"key":"181_CR29","first-page":"417","volume":"2011","author":"E Biham","year":"2011","unstructured":"Biham E, Dunkelman O, Keller N, Shamir A. New data-efficient attacks on reduced-round idea. IACR Cryptol ePrint Arch. 2011;2011:417.","journal-title":"IACR Cryptol ePrint Arch"},{"key":"181_CR30","doi-asserted-by":"publisher","DOI":"10.1201\/9781420057133","volume-title":"Cryptography: theory and practice","author":"DR Stinson","year":"2005","unstructured":"Stinson DR. Cryptography: theory and practice. Boca Raton: CRC Press; 2005."},{"key":"181_CR31","volume-title":"Handbook of applied cryptography","author":"AJ Menezes","year":"1996","unstructured":"Menezes AJ, Van Oorschot PC, Vanstone SA. Handbook of applied cryptography. Boca Raton: CRC Press; 1996."}],"updated-by":[{"DOI":"10.1007\/s42979-023-02168-3","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2023,9,28]],"date-time":"2023-09-28T00:00:00Z","timestamp":1695859200000}}],"container-title":["SN Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42979-020-00181-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s42979-020-00181-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42979-020-00181-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,28]],"date-time":"2023-09-28T09:25:27Z","timestamp":1695893127000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s42979-020-00181-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,5]]}},"alternative-id":["181"],"URL":"https:\/\/doi.org\/10.1007\/s42979-020-00181-4","relation":{},"ISSN":["2662-995X","2661-8907"],"issn-type":[{"value":"2662-995X","type":"print"},{"value":"2661-8907","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,5]]},"assertion":[{"value":"20 May 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 April 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 May 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 September 2023","order":4,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":5,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s42979-023-02168-3","URL":"https:\/\/doi.org\/10.1007\/s42979-023-02168-3","order":7,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"169"}}