{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:16Z","timestamp":1751660536098,"version":"3.40.3"},"publisher-location":"Cham","reference-count":65,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031377082"},{"type":"electronic","value":"9783031377099"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Masking is a widely-used effective countermeasure against power side-channel attacks for implementing cryptographic algorithms. Surprisingly, few formal verification techniques have addressed a fundamental question, i.e., whether the masked program and the original (unmasked) cryptographic algorithm are functional equivalent. In this paper, we study this problem for masked arithmetic programs over Galois fields of characteristic 2. We propose an automated approach based on term rewriting, aided by random testing and SMT solving. The overall approach is sound, and complete under certain conditions which do meet in practice. We implement the approach as a new tool and carry out extensive experiments on various benchmarks. The results confirm the effectiveness, efficiency and scalability of our approach. Almost all the benchmarks can be proved for the first time by the term rewriting system solely. In particular, detects a new flaw in a masked implementation published in EUROCRYPT 2017.<\/jats:p>","DOI":"10.1007\/978-3-031-37709-9_13","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"255-280","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Automated Verification of\u00a0Correctness for\u00a0Masked Arithmetic Programs"],"prefix":"10.1007","author":[{"given":"Mingyang","family":"Liu","sequence":"first","affiliation":[]},{"given":"Fu","family":"Song","sequence":"additional","affiliation":[]},{"given":"Taolue","family":"Chen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"issue":"2","key":"13_CR1","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s11334-013-0195-x","volume":"9","author":"R Affeldt","year":"2013","unstructured":"Affeldt, R.: On construction of a library of formally verified low-level arithmetic functions. Innov. Syst. Softw. Eng. 9(2), 59\u201377 (2013)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Ahman, D., et al.: Dijkstra monads for free. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 515\u2013529 (2017)","DOI":"10.1145\/3009837.3009878"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., et al.: Jasmin: high-assurance and high-speed cryptography. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp. 1807\u20131823 (2017)","DOI":"10.1145\/3133956.3134078"},{"issue":"2","key":"13_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2701415","volume":"37","author":"AW Appel","year":"2015","unstructured":"Appel, A.W.: Verification of a cryptographic primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37(2), 1\u201331 (2015)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 13243, pp. 415\u2013442 (2022). v1.0.0 is used","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Barthe, G., et al.: Strong non-interference and type-directed higher-order masking. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 116\u2013129 (2016)","DOI":"10.1145\/2976749.2978427"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1007\/978-3-319-56620-7_19","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2017","author":"G Barthe","year":"2017","unstructured":"Barthe, G., Dupressoir, F., Faust, S., Gr\u00e9goire, B., Standaert, F.-X., Strub, P.-Y.: Parallel implementations of masking schemes and the bounded moment leakage model. In: Coron, J.-S., Nielsen, J.B. (eds.) EUROCRYPT 2017. LNCS, vol. 10210, pp. 535\u2013566. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-56620-7_19"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146\u2013166. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-662-53008-5_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2016","author":"C Beierle","year":"2016","unstructured":"Beierle, C., et al.: The SKINNY family of block ciphers and its low-latency variant MANTIS. In: Robshaw, M., Katz, J. (eds.) CRYPTO 2016. LNCS, vol. 9815, pp. 123\u2013153. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53008-5_5"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"616","DOI":"10.1007\/978-3-662-49896-5_22","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2016","author":"S Bela\u00efd","year":"2016","unstructured":"Bela\u00efd, S., Benhamouda, F., Passel\u00e8gue, A., Prouff, E., Thillard, A., Vergnaud, D.: Randomness complexity of private circuits for multiplication. In: Fischlin, M., Coron, J.-S. (eds.) EUROCRYPT 2016. LNCS, vol. 9666, pp. 616\u2013648. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49896-5_22"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-319-78375-8_11","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2018","author":"R Bloem","year":"2018","unstructured":"Bloem, R., Gross, H., Iusupov, R., K\u00f6nighofer, B., Mangard, S., Winter, J.: Formal verification of masked hardware implementations in the presence of glitches. In: Nielsen, J.B., Rijmen, V. (eds.) EUROCRYPT 2018. LNCS, vol. 10821, pp. 321\u2013353. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-78375-8_11"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-540-74735-2_31","volume-title":"Cryptographic Hardware and Embedded Systems - CHES 2007","author":"A Bogdanov","year":"2007","unstructured":"Bogdanov, A., et al.: PRESENT: an ultra-lightweight block cipher. In: Paillier, P., Verbauwhede, I. (eds.) CHES 2007. LNCS, vol. 4727, pp. 450\u2013466. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74735-2_31"},{"key":"13_CR15","unstructured":"Bond, B., et al.: Vale: verifying high-performance cryptographic assembly code. In: 26th USENIX security symposium, pp. 917\u2013934 (2017)"},{"issue":"1","key":"13_CR16","doi-asserted-by":"publisher","first-page":"4","DOI":"10.5951\/MT.5.1.0004","volume":"5","author":"J Bowden","year":"1912","unstructured":"Bowden, J.: The Russian peasant method of multiplication. Math. Teach. 5(1), 4\u20138 (1912)","journal-title":"Math. Teach."},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Bronchain, O., Cassiers, G.: Bitslicing arithmetic\/Boolean masking conversions for fun and profit: with application to lattice-based KEMs. IACR Trans. Cryptograph. Hardw. Embed. Syst., 553\u2013588 (2022)","DOI":"10.46586\/tches.v2022.i4.553-588"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174\u2013177. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_16"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-642-34047-5_21","volume-title":"Fast Software Encryption","author":"C Carlet","year":"2012","unstructured":"Carlet, C., Goubin, L., Prouff, E., Quisquater, M., Rivain, M.: Higher-order masking schemes for s-boxes. In: Canteaut, A. (ed.) FSE 2012. LNCS, vol. 7549, pp. 366\u2013384. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34047-5_21"},{"issue":"10","key":"13_CR20","doi-asserted-by":"publisher","first-page":"1677","DOI":"10.1109\/TC.2020.3022979","volume":"70","author":"G Cassiers","year":"2020","unstructured":"Cassiers, G., Gr\u00e9goire, B., Levi, I., Standaert, F.X.: Hardware private circuits: from trivial composition to full verification. IEEE Trans. Comput. 70(10), 1677\u20131690 (2020)","journal-title":"IEEE Trans. Comput."},{"key":"13_CR21","doi-asserted-by":"publisher","first-page":"2542","DOI":"10.1109\/TIFS.2020.2971153","volume":"15","author":"G Cassiers","year":"2020","unstructured":"Cassiers, G., Standaert, F.X.: Trivially and efficiently composing masked gadgets with probe isolating non-interference. IEEE Trans. Inf. Forensics Secur. 15, 2542\u20132555 (2020)","journal-title":"IEEE Trans. Inf. Forensics Secur."},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-030-72013-1_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Chalupa","year":"2021","unstructured":"Chalupa, M., Ja\u0161ek, T., Nov\u00e1k, J., \u0158echt\u00e1\u010dkov\u00e1, A., \u0160okov\u00e1, V., Strej\u010dek, J.: Symbiotic 8: beyond symbolic execution. In: Groote, J.F., Larsen, K.G. (eds.) TACAS 2021. LNCS, vol. 12652, pp. 453\u2013457. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_31"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Chen, Y.F., et al.: Verifying curve25519 software. In: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, pp. 299\u2013309 (2014)","DOI":"10.1145\/2660267.2660370"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-662-43933-3_21","volume-title":"Fast Software Encryption","author":"J-S Coron","year":"2014","unstructured":"Coron, J.-S., Prouff, E., Rivain, M., Roche, T.: Higher-order side channel security and mask refreshing. In: Moriai, S. (ed.) FSE 2013. LNCS, vol. 8424, pp. 410\u2013424. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43933-3_21"},{"key":"13_CR25","unstructured":"Daemen, J., Rijmen, V.: AES proposal: Rijndael (1999)"},{"issue":"2","key":"13_CR26","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/2685616","volume":"24","author":"H Eldib","year":"2014","unstructured":"Eldib, H., Wang, C., Schaumont, P.: Formal verification of software countermeasures against side-channel attacks. ACM Trans. Softw. Eng. Methodol. 24(2), 11 (2014)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In: Proceedings of the 2019 IEEE Symposium on Security and Privacy, pp. 1202\u20131219 (2019)","DOI":"10.1109\/SP.2019.00005"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Fu, Y., Liu, J., Shi, X., Tsai, M., Wang, B., Yang, B.: Signed cryptographic program verification with typed cryptoline. In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, pp. 1591\u20131606 (2019)","DOI":"10.1145\/3319535.3354199"},{"issue":"3","key":"13_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3428015","volume":"30","author":"P Gao","year":"2021","unstructured":"Gao, P., Xie, H., Song, F., Chen, T.: A hybrid approach to formal verification of higher-order masked arithmetic programs. ACM Trans. Softw. Eng. Methodol. 30(3), 1\u201342 (2021)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"3","key":"13_CR30","first-page":"973","volume":"48","author":"P Gao","year":"2022","unstructured":"Gao, P., Xie, H., Sun, P., Zhang, J., Song, F., Chen, T.: Formal verification of masking countermeasures for arithmetic programs. IEEE Trans. Software Eng. 48(3), 973\u20131000 (2022)","journal-title":"IEEE Trans. Software Eng."},{"key":"13_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-030-17462-0_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Gao","year":"2019","unstructured":"Gao, P., Xie, H., Zhang, J., Song, F., Chen, T.: Quantitative verification of masked arithmetic programs against side-channel attacks. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 155\u2013173. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_9"},{"issue":"3","key":"13_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3330392","volume":"28","author":"P Gao","year":"2019","unstructured":"Gao, P., Zhang, J., Song, F., Wang, C.: Verifying and quantifying side-channel resistance of masked software implementations. ACM Trans. Softw. Eng. Methodol. 28(3), 1\u201332 (2019)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/3-540-48059-5_15","volume-title":"Cryptographic Hardware and Embedded Systems","author":"L Goubin","year":"1999","unstructured":"Goubin, L., Patarin, J.: DES and differential power analysis the \u201cDuplication\u2019\u2019 method. In: Ko\u00e7, \u00c7.K., Paar, C. (eds.) CHES 1999. LNCS, vol. 1717, pp. 158\u2013172. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48059-5_15"},{"key":"13_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-319-66787-4_6","volume-title":"Cryptographic Hardware and Embedded Systems \u2013 CHES 2017","author":"H Gross","year":"2017","unstructured":"Gross, H., Mangard, S.: Reconciling $$d+1$$ masking in hardware and software. In: Fischer, W., Homma, N. (eds.) CHES 2017. LNCS, vol. 10529, pp. 115\u2013136. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66787-4_6"},{"key":"13_CR35","doi-asserted-by":"crossref","unstructured":"Gro\u00df, H., Mangard, S., Korak, T.: Domain-oriented masking: compact masked hardware implementations with arbitrary protection order. Cryptology ePrint Archive (2016)","DOI":"10.1145\/2996366.2996426"},{"key":"13_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"13_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-540-45146-4_27","volume-title":"Advances in Cryptology - CRYPTO 2003","author":"Y Ishai","year":"2003","unstructured":"Ishai, Y., Sahai, A., Wagner, D.: Private circuits: securing hardware against probing attacks. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 463\u2013481. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45146-4_27"},{"key":"13_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-030-72013-1_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kaufmann","year":"2021","unstructured":"Kaufmann, D., Biere, A.: AMulet\u00a02.0 for verifying multiplier circuits. In: TACAS 2021. LNCS, vol. 12652, pp. 357\u2013364. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_19"},{"key":"13_CR39","doi-asserted-by":"crossref","unstructured":"Kaufmann, D., Biere, A., Kauers, M.: Verifying large multipliers by combining SAT and computer algebra. In: Proceedings of the 2019 Formal Methods in Computer Aided Design, pp. 28\u201336 (2019)","DOI":"10.23919\/FMCAD.2019.8894250"},{"key":"13_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-23951-9_7","volume-title":"Cryptographic Hardware and Embedded Systems \u2013 CHES 2011","author":"HS Kim","year":"2011","unstructured":"Kim, H.S., Hong, S., Lim, J.: A fast and provably secure higher-order masking of AES S-Box. In: Preneel, B., Takagi, T. (eds.) CHES 2011. LNCS, vol. 6917, pp. 95\u2013107. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23951-9_7"},{"key":"13_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/3-540-48405-1_25","volume-title":"Advances in Cryptology \u2014 CRYPTO\u2019 99","author":"P Kocher","year":"1999","unstructured":"Kocher, P., Jaffe, J., Jun, B.: Differential power analysis. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 388\u2013397. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48405-1_25"},{"key":"13_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/3-540-68697-5_9","volume-title":"Advances in Cryptology \u2014 CRYPTO \u201996","author":"PC Kocher","year":"1996","unstructured":"Kocher, P.C.: Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol. 1109, pp. 104\u2013113. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-68697-5_9"},{"key":"13_CR43","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: Proceedings of the 2nd IEEE\/ACM International Symposium on Code Generation and Optimization, pp. 75\u201386 (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"13_CR44","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"13_CR45","doi-asserted-by":"crossref","unstructured":"Liu, J., Shi, X., Tsai, M., Wang, B., Yang, B.: Verifying arithmetic in cryptographic C programs. In: Proceedings of the 34th IEEE\/ACM International Conference on Automated Software Engineering, pp. 552\u2013564 (2019)","DOI":"10.1109\/ASE.2019.00058"},{"key":"13_CR46","doi-asserted-by":"crossref","unstructured":"Luo, C., Fei, Y., Kaeli, D.R.: Effective simple-power analysis attacks of elliptic curve cryptography on embedded systems. In: Proceedings of the International Conference on Computer-Aided Design, p. 115 (2018)","DOI":"10.1145\/3240765.3240802"},{"key":"13_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"13_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-319-03545-1_5","volume-title":"Certified Programs and Proofs","author":"MO Myreen","year":"2013","unstructured":"Myreen, M.O., Curello, G.: Proof pearl: a verified Bignum implementation in x86-64 machine code. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 66\u201381. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03545-1_5"},{"key":"13_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/978-3-540-71209-1_44","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MO Myreen","year":"2007","unstructured":"Myreen, M.O., Gordon, M.J.C.: Hoare logic for realistically modelled machine\u00a0code. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 568\u2013582. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_44"},{"key":"13_CR50","unstructured":"National Institute of Standards and Technology: Data encryption standard (DES). FIPS Publication, pp. 46\u20133, October 1999"},{"key":"13_CR51","doi-asserted-by":"crossref","unstructured":"Newman, M.H.A.: On theories with a combinatorial definition of equivalence. Annals Math., 223\u2013243 (1942)","DOI":"10.2307\/1968867"},{"key":"13_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-45238-6_4","volume-title":"Cryptographic Hardware and Embedded Systems - CHES 2003","author":"SB \u00d6rs","year":"2003","unstructured":"\u00d6rs, S.B., Oswald, E., Preneel, B.: Power-analysis attacks on an FPGA \u2013 first experimental results. In: Walter, C.D., Ko\u00e7, \u00c7.K., Paar, C. (eds.) CHES 2003. LNCS, vol. 2779, pp. 35\u201350. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45238-6_4"},{"key":"13_CR53","unstructured":"Polyakov, A., Tsai, M., Wang, B., Yang, B.: Verifying arithmetic assembly programs in cryptographic primitives (invited talk). In: Proceedings of the 29th International Conference on Concurrency Theory, pp. 1\u201316 (2018)"},{"issue":"6","key":"13_CR54","doi-asserted-by":"publisher","first-page":"799","DOI":"10.1109\/TC.2009.15","volume":"58","author":"E Prouff","year":"2009","unstructured":"Prouff, E., Rivain, M., Bevan, R.: Statistical analysis of second order differential power analysis. IEEE Trans. Comput. 58(6), 799\u2013811 (2009)","journal-title":"IEEE Trans. Comput."},{"key":"13_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-319-08867-9_7","volume-title":"Computer Aided Verification","author":"Z Rakamari\u0107","year":"2014","unstructured":"Rakamari\u0107, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 106\u2013113. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_7"},{"key":"13_CR56","first-page":"948","volume":"2019","author":"P Ravi","year":"2019","unstructured":"Ravi, P., Roy, S.S., Chattopadhyay, A., Bhasin, S.: Generic side-channel attacks on CCA-secure lattice-based PKE and KEM schemes. IACR Cryptol. ePrint Arch. 2019, 948 (2019)","journal-title":"IACR Cryptol. ePrint Arch."},{"key":"13_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"764","DOI":"10.1007\/978-3-662-47989-6_37","volume-title":"Advances in Cryptology \u2013 CRYPTO 2015","author":"O Reparaz","year":"2015","unstructured":"Reparaz, O., Bilgin, B., Nikova, S., Gierlichs, B., Verbauwhede, I.: Consolidating masking schemes. In: Gennaro, R., Robshaw, M. (eds.) CRYPTO 2015. LNCS, vol. 9215, pp. 764\u2013783. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-47989-6_37"},{"key":"13_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-642-15031-9_28","volume-title":"Cryptographic Hardware and Embedded Systems, CHES 2010","author":"M Rivain","year":"2010","unstructured":"Rivain, M., Prouff, E.: Provably secure higher-order masking of AES. In: Mangard, S., Standaert, F.-X. (eds.) CHES 2010. LNCS, vol. 6225, pp. 413\u2013427. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15031-9_28"},{"key":"13_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-030-68487-7_8","volume-title":"Smart Card Research and Advanced Applications","author":"T Schamberger","year":"2021","unstructured":"Schamberger, T., Renner, J., Sigl, G., Wachter-Zeh, A.: A power side-channel attack on the CCA2-secure HQC KEM. In: Liardet, P.-Y., Mentens, N. (eds.) CARDIS 2020. LNCS, vol. 12609, pp. 119\u2013134. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-68487-7_8"},{"issue":"11","key":"13_CR60","doi-asserted-by":"publisher","first-page":"612","DOI":"10.1145\/359168.359176","volume":"22","author":"A Shamir","year":"1979","unstructured":"Shamir, A.: How to share a secret. Commun. ACM 22(11), 612\u2013613 (1979)","journal-title":"Commun. ACM"},{"issue":"6","key":"13_CR61","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. Priv. 14(6), 26\u201333 (2016)","journal-title":"IEEE Secur. Priv."},{"key":"13_CR62","doi-asserted-by":"crossref","unstructured":"Tsai, M.H., Wang, B.Y., Yang, B.Y.: Certified verification of algebraic properties on low-level mathematical constructs in cryptographic programs. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp. 1973\u20131987 (2017)","DOI":"10.1145\/3133956.3134076"},{"key":"13_CR63","volume-title":"Elements of Number Theory","author":"IM Vinogradov","year":"2016","unstructured":"Vinogradov, I.M.: Elements of Number Theory. Courier Dover Publications, New York (2016)"},{"key":"13_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-319-96142-2_12","volume-title":"Computer Aided Verification","author":"J Zhang","year":"2018","unstructured":"Zhang, J., Gao, P., Song, F., Wang, C.: SCInfer: refinement-based verification of software countermeasures against side-channel attacks. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 157\u2013177. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_12"},{"key":"13_CR65","doi-asserted-by":"crossref","unstructured":"Zinzindohou\u00e9, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: A verified modern cryptographic library. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp. 1789\u20131806 (2017)","DOI":"10.1145\/3133956.3134043"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37709-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,24]],"date-time":"2024-10-24T06:56:48Z","timestamp":1729753008000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37709-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377082","9783031377099"],"references-count":65,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37709-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}