{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,11]],"date-time":"2026-07-11T17:14:41Z","timestamp":1783790081475,"version":"3.55.0"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711763","type":"print"},{"value":"9783031711770","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Fault injection attack is a class of active, physical attacks against cryptographic circuits. The design and implementation of countermeasures against such attacks are intricate, error-prone and laborious, necessitating formal verification to guarantee their correctness. In this paper, we propose the first compositional verification approach for round-based hardware implementations of cryptographic algorithms. Our approach decomposes a circuit into a set of single-round sub-circuits which are verified individually by either SAT\/SMT- or BDD-based tools. Our approach is implemented as an open-source tool , which is evaluated extensively on realistic cryptographic circuit benchmarks. The experimental results show that our approach is significantly more effective and efficient than the state-of-the-art.<\/jats:p>","DOI":"10.1007\/978-3-031-71177-0_13","type":"book-chapter","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:10:51Z","timestamp":1726121451000},"page":"189-207","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Compositional Verification of\u00a0Cryptographic Circuits Against Fault Injection Attacks"],"prefix":"10.1007","author":[{"given":"Huiyu","family":"Tan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xi","family":"Yang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fu","family":"Song","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Taolue","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhilin","family":"Wu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,9,13]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1109\/TC.2019.2948617","volume":"69","author":"A Aghaie","year":"2020","unstructured":"Aghaie, A., Moradi, A., Rasoolzadeh, S., Shahmirzadi, A.R., Schellenberg, F., Schneider, T.: Impeccable circuits. IEEE Trans. Comput. 69, 361\u2013376 (2020)","journal-title":"IEEE Trans. Comput."},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Agoyan, M., Dutertre, J., Naccache, D., Robisson, B., Tria, A.: When clocks fail: on critical paths and clock faults. In: Proceedings of the 9th IFIP WG 8.8\/11.2 International Conference (CARDIS), pp. 182\u2013193 (2010)","DOI":"10.1007\/978-3-642-12510-2_13"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Anderson, R.J., Kuhn, M.G.: Low cost attacks on tamper resistant devices. In: Christianson, B., Crispo, B., Lomas, T.M.A., Roe, M. (eds.) Proceedings of the 5th International Workshop on Security Protocols, vol.\u00a01361, pp. 125\u2013136 (1997). https:\/\/doi.org\/10.1007\/BFB0028165","DOI":"10.1007\/BFB0028165"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Arribas, V., Wegener, F., Moradi, A., Nikova, S.: Cryptographic fault diagnosis using VerFI. In: Proceedings of the IEEE International Symposium on Hardware Oriented Security and Trust (HOST), pp. 229\u2013240 (2020)","DOI":"10.1109\/HOST45689.2020.9300264"},{"issue":"15","key":"13_CR5","doi-asserted-by":"publisher","first-page":"2787","DOI":"10.1016\/j.comnet.2010.05.010","volume":"54","author":"L Atzori","year":"2010","unstructured":"Atzori, L., Iera, A., Morabito, G.: The internet of things: a survey. Comput. Netw. 54(15), 2787\u20132805 (2010)","journal-title":"Comput. Netw."},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Audemard, G., Simon, L.: On the glucose SAT solver. Int. J. Artif. Intell. Tools 27(1), 1840001:1\u20131840001:25 (2018)","DOI":"10.1142\/S0218213018400018"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Azarbad, M.R., Alizadeh, B.: Scalable SMT-based equivalence checking of nested loop pipelining in behavioral synthesis. ACM Trans. Design Autom. Electr. Syst. 22(2), 22:1\u201322:22 (2017)","DOI":"10.1145\/2953879"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Baksi, A.: Classical and Physical Security of Symmetric Key Cryptographic Algorithms. Springer, Singapore (2022). https:\/\/doi.org\/10.1007\/978-981-16-6522-6","DOI":"10.1007\/978-981-16-6522-6"},{"issue":"2","key":"13_CR9","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1109\/JPROC.2005.862424","volume":"94","author":"H Bar-El","year":"2006","unstructured":"Bar-El, H., Choukri, H., Naccache, D., Tunstall, M., Whelan, C.: The sorcerer\u2019s apprentice guide to fault attacks. Proc. IEEE 94(2), 370\u2013382 (2006). https:\/\/doi.org\/10.1109\/JPROC.2005.862424","journal-title":"Proc. IEEE"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of the 36th Conference on Design Automation (DAC), pp. 317\u2013320 (1999)","DOI":"10.1145\/309847.309942"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp. 193\u2013207 (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., et al.: A lazy and layered SMT($$\\cal{BV}$$) solver for hard industrial verification problems. In: Proceedings of the 19th International Conference on Computer Aided Verification (CAV), pp. 547\u2013560 (2007)","DOI":"10.1007\/978-3-540-73368-3_54"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E., McMillan, K.L., Dill, D.L.: Symbolic model checking for sequential circuit verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 13(4), 401\u2013424 (1994)","DOI":"10.1109\/43.275352"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10$${\\hat{\\,}}$$20 states and beyond. In: Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS), pp. 428\u2013439 (1990)","DOI":"10.1109\/LICS.1990.113767"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Dehbaoui, A., Dutertre, J., Robisson, B., Tria, A.: Electromagnetic transient faults injection on a hardware and a software implementations of AES. In: Proceedings of the Workshop on Fault Diagnosis and Tolerance in Cryptography (FDTC), pp. 7\u201315 (2012)","DOI":"10.1109\/FDTC.2012.15"},{"key":"13_CR17","unstructured":"van Eijk, C.A.J.: Sequential equivalence checking without state space traversal. In: Proceedings of Design, Automation and Test in Europe (DATE), pp. 618\u2013623 (1998)"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Eldib, H., Wu, M., Wang, C.: Synthesis of fault-attack countermeasures for cryptographic circuits. In: Proceedings of the 28th International Conference on Computer Aided Verification (CAV), pp. 343\u2013363 (2016)","DOI":"10.1007\/978-3-319-41540-6_19"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Gao, P., Song, F., Chen, T.: Compositional verification of first-order masking countermeasures against power side-channel attacks. ACM Trans. Softw. Eng. Methodol. 33(3), 79:1\u201379:38 (2024)","DOI":"10.1145\/3635707"},{"issue":"OOPSLA2","key":"13_CR20","doi-asserted-by":"publisher","first-page":"1817","DOI":"10.1145\/3622862","volume":"7","author":"P Gao","year":"2023","unstructured":"Gao, P., Zhang, Y., Song, F., Chen, T., Standaert, F.: Compositional verification of efficient masking countermeasures against side-channel attacks. Proc. ACM Program. Lang. 7(OOPSLA2), 1817\u20131847 (2023). https:\/\/doi.org\/10.1145\/3622862","journal-title":"Proc. ACM Program. Lang."},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Joye, M., Tunstall, M. (eds.) Fault Analysis in Cryptography. Information Security and Cryptography. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29656-7","DOI":"10.1007\/978-3-642-29656-7"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Kaiss, D., Skaba, M., Hanna, Z., Khasidashvili, Z.: Industrial strength SAT-based alignability algorithm for hardware equivalence verification. In: Proceedings of the 7th International Conference on Formal Methods in Computer-Aided Design, pp. 20\u201326 (2007)","DOI":"10.1109\/FAMCAD.2007.37"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Khanna, P., Rebeiro, C., Hazra, A.: XfC: a framework for exploitable fault characterization in block ciphers. In: Proceedings of the 54th Annual Design Automation Conference (DAC), pp.\u00a01\u20136 (2017)","DOI":"10.1145\/3061639.3062340"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Khasidashvili, Z., Skaba, M., Kaiss, D., Hanna, Z.: Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints. In: Proceedings of the International Conference on Computer-Aided Design, pp. 58\u201365 (2004)","DOI":"10.1109\/ICCAD.2004.1382543"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Khasidashvili, Z., Skaba, M., Kaiss, D., Hanna, Z.: Post-reboot equivalence and compositional verification of hardware. In: Proceedings of the 6th International Conference on Formal Methods in Computer-Aided Design, pp. 11\u201318 (2006)","DOI":"10.1109\/FMCAD.2006.25"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Malkin, T., Standaert, F., Yung, M.: A comparative cost\/security analysis of fault attack countermeasures. In: Proceedings of the 3rd International Workshop on Fault Diagnosis and Tolerance in Cryptography, pp. 159\u2013172 (2006)","DOI":"10.1007\/11889700_15"},{"issue":"1\u20133","key":"13_CR27","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S0167-6423(99)00030-1","volume":"37","author":"KL McMillan","year":"2000","unstructured":"McMillan, K.L.: A methodology for hardware verification using compositional model checking. Sci. Comput. Program. 37(1\u20133), 279\u2013309 (2000). https:\/\/doi.org\/10.1016\/S0167-6423(99)00030-1","journal-title":"Sci. Comput. Program."},{"key":"13_CR28","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla at the SMT-COMP 2020. CoRR abs\/2006.01621 (2020). https:\/\/arxiv.org\/abs\/2006.01621"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Pixley, C.: A theory and implementation of sequential hardware equivalence. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 11(12), 1469\u20131478 (1992)","DOI":"10.1109\/43.180261"},{"key":"13_CR30","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1109\/TC.2022.3164259","volume":"72","author":"J Richter-Brockmann","year":"2023","unstructured":"Richter-Brockmann, J., Sasdrich, P., G\u00fcneysu, T.: Revisiting fault adversary models - hardware faults in theory and practice. IEEE Trans. Comput. 72, 572\u2013585 (2023)","journal-title":"IEEE Trans. Comput."},{"key":"13_CR31","doi-asserted-by":"publisher","first-page":"447","DOI":"10.46586\/tches.v2021.i4.447-473","volume":"2021","author":"J Richter-Brockmann","year":"2021","unstructured":"Richter-Brockmann, J., Shahmirzadi, A.R., Sasdrich, P., Moradi, A., G\u00fcneysu, T.: Fiver - robust verification of countermeasures against fault injections. IACR Trans. Cryptographic Hardware Embed. Syst. 2021, 447\u2013473 (2021)","journal-title":"IACR Trans. Cryptographic Hardware Embed. Syst."},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"Roy, I., Rebeiro, C., Hazra, A., Bhunia, S.: SAFARI: automatic synthesis of fault-attack resistant block cipher implementations. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39(4), 752\u2013765 (2020)","DOI":"10.1109\/TCAD.2019.2897629"},{"issue":"2","key":"13_CR33","doi-asserted-by":"publisher","first-page":"242","DOI":"10.46586\/tches.v2018.i2.242-276","volume":"2018","author":"S Saha","year":"2018","unstructured":"Saha, S., Mukhopadhyay, D., Dasgupta, P.: ExpFault: an automated framework for exploitable fault characterization in block ciphers. IACR Trans. Cryptographic Hardware Embed. Syst. 2018(2), 242\u2013276 (2018)","journal-title":"IACR Trans. Cryptographic Hardware Embed. Syst."},{"key":"13_CR34","doi-asserted-by":"crossref","unstructured":"Selmane, N., Guilley, S., Danger, J.: Practical setup time violation attacks on AES. In: Proceedings of the 7th European Dependable Computing Conference (EDCC), pp. 91\u201396 (2008)","DOI":"10.1109\/EDCC-7.2008.11"},{"key":"13_CR35","doi-asserted-by":"crossref","unstructured":"Shahmirzadi, A.R., Rasoolzadeh, S., Moradi, A.: Impeccable circuits II. Proceedings of the 57th ACM\/IEEE Design Automation Conference (DAC), pp.\u00a01\u20136 (2020)","DOI":"10.1109\/DAC18072.2020.9218615"},{"key":"13_CR36","doi-asserted-by":"crossref","unstructured":"Skorobogatov, S.P., Anderson, R.J.: Optical fault induction attacks. In: Proceedings of the 4th International Workshop Redwood Shores on Cryptographic Hardware and Embedded Systems (CHES), pp. 2\u201312 (2003)","DOI":"10.1007\/3-540-36400-5_2"},{"key":"13_CR37","unstructured":"Tan, H., Gao, P., Chen, T., Song, F., Wu, Z.: SAT-based formal fault-resistance verification of cryptographic circuits. CoRR abs\/2307.00561 (2023)"},{"key":"13_CR38","unstructured":"Tan, H., Gao, P., Chen, T., Song, F., Wu, Z.: CLEAVE (2024). https:\/\/github.com\/S3L-official\/CLEAVE"},{"key":"13_CR39","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1016\/j.iotcps.2021.12.002","volume":"1","author":"AK Tyagi","year":"2021","unstructured":"Tyagi, A.K., Sreenath, N.: Cyber physical systems: analyses, challenges and possible solutions. Internet Things Cyber-Phys. Syst. 1, 22\u201333 (2021)","journal-title":"Internet Things Cyber-Phys. Syst."},{"issue":"3","key":"13_CR40","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1109\/TCAD.2021.3063998","volume":"41","author":"H Wang","year":"2021","unstructured":"Wang, H., Li, H., Rahman, F., Tehranipoor, M.M., Farahmandi, F.: SoFI: security property-driven vulnerability assessments of ICs against fault-injection attacks. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(3), 452\u2013465 (2021)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"13_CR41","doi-asserted-by":"crossref","unstructured":"Zussa, L., Dutertre, J.M., Clediere, J., Tria, A.: Power supply glitch induced faults on fpga: An in-depth analysis of the injection mechanism. In: Proceedings of the IEEE 19th International On-Line Testing Symposium (IOLTS), pp. 110\u2013115 (2013)","DOI":"10.1109\/IOLTS.2013.6604060"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71177-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T01:09:57Z","timestamp":1732756197000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71177-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,13]]},"ISBN":["9783031711763","9783031711770"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71177-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,13]]},"assertion":[{"value":"13 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}