{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:16:25Z","timestamp":1763468185895},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642548611"},{"type":"electronic","value":"9783642548628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54862-8_5","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T13:33:34Z","timestamp":1395408814000},"page":"62-77","source":"Crossref","is-referenced-by-count":27,"title":["SMT-Based Verification of Software Countermeasures against Side-Channel Attacks"],"prefix":"10.1007","author":[{"given":"Hassan","family":"Eldib","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Schaumont","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-642-27954-6_2","volume-title":"Topics in Cryptology \u2013 CT-RSA 2012","author":"J. Balasch","year":"2012","unstructured":"Balasch, J., Gierlichs, B., Verdult, R., Batina, L., Verbauwhede, I.: Power analysis of Atmel CryptoMemory \u2013 recovering keys from secure EEPROMs. In: Dunkelman, O. (ed.) CT-RSA 2012. LNCS, vol.\u00a07178, pp. 19\u201334. Springer, Heidelberg (2012)"},{"key":"5_CR2","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":"A.G. 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.\u00a08086, pp. 293\u2013310. Springer, Heidelberg (2013)"},{"key":"5_CR3","unstructured":"Bertoni, G., Daemen, J., Peeters, M., Assche, G.V., Keer, R.V.: Keccak implementation overview, \n                    \n                      https:\/\/2.zoppoz.workers.dev:443\/http\/keccak.neokeon.org\/Keccak-implementation-3.2.pdf"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-30564-4_5","volume-title":"Selected Areas in Cryptography","author":"J. Bl\u00f6mer","year":"2004","unstructured":"Bl\u00f6mer, J., Guajardo, J., Krummel, V.: Provably secure masking of AES. In: Handschuh, H., Hasan, M.A. (eds.) SAC 2004. LNCS, vol.\u00a03357, pp. 69\u201383. Springer, Heidelberg (2004)"},{"key":"5_CR5","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-44709-1_2","volume-title":"Cryptographic Hardware and Embedded Systems - CHES 2001","author":"L. Goubin","year":"2001","unstructured":"Goubin, L.: A sound method for switching between boolean and arithmetic masking. In: Ko\u00e7, \u00c7.K., Naccache, D., Paar, C. (eds.) CHES 2001. LNCS, vol.\u00a02162, pp. 3\u201315. Springer, Heidelberg (2001)"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/11767480_16","volume-title":"Applied Cryptography and Network Security","author":"C. Herbst","year":"2006","unstructured":"Herbst, C., Oswald, E., Mangard, S.: An AES smart card implementation resistant to power analysis attacks. In: Zhou, J., Yung, M., Bao, F. (eds.) ACNS 2006. LNCS, vol.\u00a03989, pp. 239\u2013252. Springer, Heidelberg (2006)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/11545262_22","volume-title":"Cryptographic Hardware and Embedded Systems \u2013 CHES 2005","author":"M. Joye","year":"2005","unstructured":"Joye, M., Paillier, P., Schoenmakers, B.: On second-order differential power analysis. In: Rao, J.R., Sunar, B. (eds.) CHES 2005. LNCS, vol.\u00a03659, pp. 293\u2013308. Springer, Heidelberg (2005)"},{"key":"5_CR10","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":"P.C. Kocher","year":"1999","unstructured":"Kocher, P.C., Jaffe, J., Jun, B.: Differential power analysis. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol.\u00a01666, pp. 388\u2013397. Springer, Heidelberg (1999)"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Li, B., Wang, C., Somenzi, F.: A satisfiability-based approach to abstraction refinement in model checking. Electronic Notes in Theoretical Computer Science\u00a089(4) (2003)","DOI":"10.1016\/S1571-0661(05)82546-0"},{"key":"5_CR12","unstructured":"Mangard, S., Oswald, E., Popp, T.: Power Analysis Attacks - Revealing the Secrets of Smart Cards. Springer (2007)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/3-540-44706-7_11","volume-title":"Fast Software Encryption","author":"T.S. Messerges","year":"2001","unstructured":"Messerges, T.S.: Securing the AES finalists against power analysis attacks. In: Schneier, B. (ed.) FSE 2000. LNCS, vol.\u00a01978, pp. 150\u2013164. Springer, Heidelberg (2001)"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Moradi, A., Barenghi, A., Kasper, T., Paar, C.: On the vulnerability of FPGA bitstream encryption against power analysis attacks: Extracting keys from Xilinx Virtex-II FPGAs. In: ACM Conference on Computer and Communications Security, pp. 111\u2013124 (2011)","DOI":"10.1145\/2046707.2046722"},{"key":"5_CR15","unstructured":"NIST. Keccak reference code submission to NIST\u2019s SHA-3 competition (Round 3), \n                    \n                      https:\/\/2.zoppoz.workers.dev:443\/http\/csrc.nist.gov\/groups\/ST\/hash\/sha-3\/Round3\/documents\/Keccak_FinalRnd.zip"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Paar, C., Eisenbarth, T., Kasper, M., Kasper, T., Moradi, A.: Keeloq and side-channel analysis-evolution of an attack. In: FDTC, pp. 65\u201369 (2009)","DOI":"10.1109\/FDTC.2009.44"},{"key":"5_CR17","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.\u00a07881, pp. 142\u2013159. Springer, Heidelberg (2013)"},{"issue":"1","key":"5_CR18","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\u00a021(1), 5\u201319 (2003)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-642-41383-4_5","volume-title":"Advances in Information and Computer Security","author":"M. Taha","year":"2013","unstructured":"Taha, M., Schaumont, P.: Differential power analysis of MAC-Keccak at any key-length. In: Sakiyama, K., Terada, M. (eds.) IWSEC 2013. LNCS, vol.\u00a08231, pp. 68\u201382. Springer, Heidelberg (2013)"},{"key":"5_CR20","unstructured":"Wang, C., Hachhtel, G.D., Somenzi, F.: Abstraction Refinement for Large Scale Model Checking. Springer (2006)"},{"key":"5_CR21","unstructured":"Yang, Z., Wang, C., Ivan\u010di\u0107, F., Gupta, A.: Mixed symbolic representations for model checking software programs. In: Formal Methods and Models for Codesign, pp. 17\u201324 (July 2006)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54862-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T11:58:19Z","timestamp":1558871899000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/link.springer.com\/10.1007\/978-3-642-54862-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548611","9783642548628"],"references-count":21,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-642-54862-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}