{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,27]],"date-time":"2026-10-27T12:02:48Z","timestamp":1793102568109,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662467992","type":"print"},{"value":"9783662468005","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46800-5_18","type":"book-chapter","created":{"date-parts":[[2015,4,13]],"date-time":"2015-04-13T04:29:09Z","timestamp":1428899349000},"page":"457-485","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":113,"title":["Verified Proofs of Higher-Order Masking"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sonia","family":"Bela\u00efd","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fran\u00e7ois","family":"Dupressoir","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pierre-Alain","family":"Fouque","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,4,14]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Akinyele, J., Barthe, G., Gr\u00e9goire, B., Schmidt, B., Strub, P.-Y.: Certified synthesis of efficient batch verifiers. In: 27th IEEE Computer Security Foundations Symposium, CSF 2014. IEEE Computer Society (2014) (to appear)","DOI":"10.1109\/CSF.2014.19"},{"key":"18_CR2","unstructured":"Balasch, J., Gierlichs, B., Grosso, V., Reparaz, O., Standaert, F.-X.: On the cost of lazy engineering for masked software implementations. Cryptology ePrint Archive, Report 2014\/413 (2014). \n                      http:\/\/eprint.iacr.org\/2014\/413"},{"key":"18_CR3","unstructured":"Barthe, G., Bela\u00efd, S., Dupressoir, F., Fouque, P.-A., Gr\u00e9goire, B., Strub, P.-Y.: Verified proofs of higher-order masking. Cryptology ePrint Archive, Report 2015\/060 (2015). \n                      http:\/\/eprint.iacr.org\/"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., Crespo, J.M., Gulwani, S., Kunz, C., Marron, M.: From relational verification to SIMD loop synthesis. In: Nicolau, A., Shen, X., Amarasinghe, S.P., Vuduc, R.W. (eds.) Principles and Practice of Parallel Programming (PPoPP), pp. 123\u2013134. ACM (2013)","DOI":"10.1145\/2442516.2442529"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-17511-4_4","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Barthe","year":"2010","unstructured":"Barthe, G., Daubignard, M., Kapron, B., Lakhnech, Y., Laporte, V.: On the equality of probabilistic terms. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16. LNCS, vol. 6355, pp. 46\u201363. Springer, Heidelberg (2010)"},{"key":"18_CR6","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.: \n                      \n                        \n                      \n                      $$\\sf EasyCrypt$$\n                    : a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD VII. LNCS, vol. 8604, pp. 146\u2013166. Springer, Heidelberg (2014)"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-22792-9_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2011","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., Zanella-B\u00e9guelin, S.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71\u201390. Springer, Heidelberg (2011)"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Zanella-B\u00e9guelin, S.: Formal certification of code-based cryptographic proofs. In: 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 90\u2013101. ACM (2009)","DOI":"10.1145\/1480881.1480894"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-642-40349-1_17","volume-title":"Cryptographic Hardware and Embedded Systems - CHES 2013","author":"AG Bayrak","year":"2013","unstructured":"Bayrak, A.G., Regazzoni, F., Novo, D., Ienne, P.: Sleuth: automated verification of software power analysis countermeasures. In: Bertoni, G., Coron, J.-S. (eds.) CHES 2013. LNCS, vol. 8086, pp. 293\u2013310. Springer, Heidelberg (2013)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-540-68914-0_27","volume-title":"Applied Cryptography and Network Security","author":"D Canright","year":"2008","unstructured":"Canright, D., Batina, L.: A very compact \u201cperfectly masked\u201d S-box for AES. In: Bellovin, S.M., Gennaro, R., Keromytis, A.D., Yung, M. (eds.) ACNS 2008. LNCS, vol. 5037, pp. 446\u2013459. Springer, Heidelberg (2008)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/3-540-48405-1_26","volume-title":"Advances in Cryptology - CRYPTO \u201999","author":"S Chari","year":"1999","unstructured":"Chari, S., Jutla, C.S., Rao, J.R., Rohatgi, P.: Towards sound approaches to counteract power-analysis attacks. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 398\u2013412. Springer, Heidelberg (1999)"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-74735-2_3","volume-title":"Cryptographic Hardware and Embedded Systems - CHES 2007","author":"J-S Coron","year":"2007","unstructured":"Coron, J.-S., Prouff, E., Rivain, M.: Side channel cryptanalysis of a higher order masking scheme. In: Paillier, P., Verbauwhede, I. (eds.) CHES 2007. LNCS, vol. 4727, pp. 28\u201344. Springer, Heidelberg (2007)"},{"key":"18_CR13","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)"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-642-55220-5_24","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2014","author":"A Duc","year":"2014","unstructured":"Duc, A., Dziembowski, S., Faust, S.: Unifying leakage models: from probing attacks to noisy leakage. In: Nguyen, P.Q., Oswald, E. (eds.) EUROCRYPT 2014. LNCS, vol. 8441, pp. 423\u2013440. Springer, Heidelberg (2014)"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-319-08867-9_8","volume-title":"Computer Aided Verification","author":"H Eldib","year":"2014","unstructured":"Eldib, H., Wang, C.: Synthesis of masking countermeasures against side channel attacks. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 114\u2013130. Springer, Heidelberg (2014)"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-642-54862-8_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Eldib","year":"2014","unstructured":"Eldib, H., Wang, C., Schaumont, P.: SMT-based verification of software countermeasures against side-channel attacks. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 62\u201377. Springer, Heidelberg (2014)"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Eldib, H., Wang, C., Taha, M.M.I., Schaumont, P.: QMS: evaluating the side-channel resistance of masked software from source code. In: The 51st Annual Design Automation Conference 2014, DAC 2014, San Francisco, CA, USA, June 1\u20135, pp. 1\u20136. ACM (2014)","DOI":"10.1109\/DAC.2014.6881536"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-13190-5_7","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2010","author":"S Faust","year":"2010","unstructured":"Faust, S., Rabin, T., Reyzin, L., Tromer, E., Vaikuntanathan, V.: Protecting circuits from leakage: the computationally-bounded and noisy cases. In: Gilbert, H. (ed.) EUROCRYPT 2010. LNCS, vol. 6110, pp. 135\u2013156. Springer, Heidelberg (2010)"},{"key":"18_CR19","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman (1979)"},{"key":"18_CR20","unstructured":"Gomes, C.P., Sabharwal, A., Selman, B.: Model counting. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 633\u2013654. IOS Press (2009)"},{"key":"18_CR21","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)"},{"key":"18_CR22","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 - CRYPTO \u201999","author":"PC Kocher","year":"1999","unstructured":"Kocher, P.C., Jaffe, J., Jun, B.: Differential power analysis. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 388\u2013397. Springer, Heidelberg (1999)"},{"key":"18_CR23","unstructured":"Mangard, S., Oswald, E., Popp, T.: Power analysis attacks - revealing the secrets of smart cards. Springer (2007)"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-24638-1_16","volume-title":"Theory of Cryptography","author":"S Micali","year":"2004","unstructured":"Micali, S., Reyzin, L.: Physically observable cryptography (extended abstract). In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 278\u2013296. Springer, Heidelberg (2004)"},{"key":"18_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-33027-8_4","volume-title":"Cryptographic Hardware and Embedded Systems \u2013 CHES 2012","author":"A Moss","year":"2012","unstructured":"Moss, A., Oswald, E., Page, D., Tunstall, M.: Compiler assisted masking. In: Prouff, E., Schaumont, P. (eds.) CHES 2012. LNCS, vol. 7428, pp. 58\u201375. Springer, Heidelberg (2012)"},{"key":"18_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/11967668_16","volume-title":"Topics in Cryptology \u2013 CT-RSA 2007","author":"E Oswald","year":"2007","unstructured":"Oswald, E., Mangard, S.: Template attacks on masking\u2014resistance is futile. In: Abe, M. (ed.) CT-RSA 2007. LNCS, vol. 4377, pp. 243\u2013256. Springer, Heidelberg (2007)"},{"key":"18_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/11502760_28","volume-title":"Fast Software Encryption","author":"E Oswald","year":"2005","unstructured":"Oswald, E., Mangard, S., Pramstaller, N., Rijmen, V.: A side-channel analysis resistant description of the AES S-box. In: Gilbert, H., Handschuh, H. (eds.) FSE 2005. LNCS, vol. 3557, pp. 413\u2013423. Springer, Heidelberg (2005)"},{"key":"18_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/11545262_23","volume-title":"Cryptographic Hardware and Embedded Systems \u2013 CHES 2005","author":"E Peeters","year":"2005","unstructured":"Peeters, E., Standaert, F.-X., Donckers, N., Quisquater, J.-J.: Improved higher-order side-channel attacks with FPGA experiments. In: Rao, J.R., Sunar, B. (eds.) CHES 2005. LNCS, vol. 3659, pp. 309\u2013323. Springer, Heidelberg (2005)"},{"key":"18_CR29","unstructured":"Pettai, M., Laud, P.: Automatic proofs of privacy of secure multi-party computation protocols against active adversaries. Cryptology ePrint Archive, Report 2014\/240 (2014). \n                      http:\/\/eprint.iacr.org\/2014\/240"},{"key":"18_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-38348-9_9","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2013","author":"E Prouff","year":"2013","unstructured":"Prouff, E., Rivain, M.: Masking against side-channel attacks: a formal security proof. In: Johansson, T., Nguyen, P.Q. (eds.) EUROCRYPT 2013. LNCS, vol. 7881, pp. 142\u2013159. Springer, Heidelberg (2013)"},{"key":"18_CR31","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)"},{"issue":"1","key":"18_CR32","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5\u201319 (2003)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"18_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/11605805_14","volume-title":"Topics in Cryptology \u2013 CT-RSA 2006","author":"K Schramm","year":"2006","unstructured":"Schramm, K., Paar, C.: Higher order masking of the AES. In: Pointcheval, D. (ed.) CT-RSA 2006. LNCS, vol. 3860, pp. 208\u2013225. Springer, Heidelberg (2006)"},{"key":"18_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-662-45611-8_15","volume-title":"Advances in Cryptology \u2013 ASIACRYPT 2014","author":"N Veyrat-Charvillon","year":"2014","unstructured":"Veyrat-Charvillon, N., G\u00e9rard, B., Standaert, F.-X.: Soft analytical side-channel attacks. In: Sarkar, P., Iwata, T. (eds.) ASIACRYPT 2014, PART I. LNCS, vol. 8873, pp. 282\u2013296. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Advances in Cryptology -- EUROCRYPT 2015"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46800-5_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T17:26:12Z","timestamp":1559150772000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46800-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662467992","9783662468005"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46800-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"14 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}