{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,7]],"date-time":"2026-05-07T11:42:42Z","timestamp":1778154162681,"version":"3.51.4"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2014,2,19]],"date-time":"2014-02-19T00:00:00Z","timestamp":1392768000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Cryptogr Eng"],"published-print":{"date-parts":[[2014,9]]},"DOI":"10.1007\/s13389-014-0077-7","type":"journal-article","created":{"date-parts":[[2014,2,18]],"date-time":"2014-02-18T16:20:59Z","timestamp":1392740459000},"page":"145-156","source":"Crossref","is-referenced-by-count":66,"title":["Formal verification of a software countermeasure against instruction skip attacks"],"prefix":"10.1007","volume":"4","author":[{"given":"N.","family":"Moro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K.","family":"Heydemann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"E.","family":"Encrenaz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"B.","family":"Robisson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,2,19]]},"reference":[{"key":"77_CR1","unstructured":"ARM: ARM Architecture Reference Manual\u2014Thumb-2 Supplement (2005)"},{"key":"77_CR2","doi-asserted-by":"crossref","unstructured":"Balasch, J., Gierlichs, B., Verbauwhede, I.: An in-depth and black-box characterization of the effects of clock glitches on 8-bit MCUs. In: 2011 Workshop on Fault Diagnosis and Tolerance in Cryptography. IEEE (2011). doi: 10.1109\/FDTC.2011.9","DOI":"10.1109\/FDTC.2011.9"},{"key":"77_CR3","doi-asserted-by":"crossref","unstructured":"Bar-El, H., Choukri, H., Naccache, D., Tunstall, M., Whelan, C.: The Sorcerer\u2019s Apprentice guide to fault attacks. In: Proceedings of the IEEE 94 (2006). doi: 10.1109\/JPROC.2005.862424","DOI":"10.1109\/JPROC.2005.862424"},{"key":"77_CR4","doi-asserted-by":"crossref","unstructured":"Barenghi, A., Bertoni, G.M., Breveglieri, L., Pelliccioli, M., Pelosi, G.: Injection technologies for fault attacks on microprocessors. In: Joye, M., Tunstall, M. (eds.) Fault Analysis in Cryptography, Information Security and Cryptography, pp. 275\u2013293. Springer, Berlin (2012). doi: 10.1007\/978-3-642-29656-7","DOI":"10.1007\/978-3-642-29656-7"},{"issue":"11","key":"77_CR5","doi-asserted-by":"crossref","first-page":"3056","DOI":"10.1109\/JPROC.2012.2188769","volume":"100","author":"A Barenghi","year":"2012","unstructured":"Barenghi, A., Breveglieri, L., Koren, I., Naccache, D.: Fault injection attacks on cryptographic devices: theory, practice, and countermeasures. Proc. IEEE 100(11), 3056\u20133076 (2012). doi: 10.1109\/JPROC.2012.2188769","journal-title":"Proc. IEEE"},{"key":"77_CR6","doi-asserted-by":"crossref","unstructured":"Barenghi, A., Breveglieri, L., Koren, I., Pelosi, G., Regazzoni, F.: Countermeasures against fault attacks on software implemented AES. In: Proceedings of the 5th Workshop on Embedded Systems Security\u2014WESS \u201910. ACM Press, New York (2010). doi: 10.1145\/1873548.1873555","DOI":"10.1145\/1873548.1873555"},{"key":"77_CR7","doi-asserted-by":"crossref","unstructured":"Boneh, D., DeMillo, R., Lipton, R.: On the importance of checking cryptographic protocols for faults. In: Advances in Cryptology\u2014EUROCRYPT \u201997, Lecture Notes in Computer Science, vol. 1233, pp. 37\u201351. Springer, Berlin (1997). doi: 10.1007\/3-540-69053-0_4","DOI":"10.1007\/3-540-69053-0_4"},{"key":"77_CR8","doi-asserted-by":"crossref","unstructured":"Chetali, B., Nguyen, Q.H.: Industrial use of formal methods for a high-level security evaluation. FM 2008: Formal Methods. Lecture Notes in Computer Science, vol. 5014, pp. 198\u2013213. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-68237-0_15"},{"key":"77_CR9","doi-asserted-by":"crossref","unstructured":"Christofi, M., Chetali, B., Goubin, L., Vigilant, D.: Formal verification of a CRT-RSA implementation against fault attacks. J. Cryptogr. Eng. (2013). doi: 10.1007\/s13389-013-0049-3","DOI":"10.1007\/s13389-013-0049-3"},{"key":"77_CR10","doi-asserted-by":"crossref","unstructured":"Dehbaoui, A., Dutertre, J.M., Robisson, B., Tria, A.: Electromagnetic transient faults injection on a hardware and a software implementations of AES. In: FDTC 2012. IEEE (2012). doi: 10.1109\/FDTC.2012.15","DOI":"10.1109\/FDTC.2012.15"},{"key":"77_CR11","doi-asserted-by":"crossref","unstructured":"Fox, A., Myreen, M.: A trustworthy monadic formalization of the armv7 instruction set architecture. Interactive Theorem Proving. Lecture Notes in Computer Science, vol. 6172, pp. 243\u2013258. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"77_CR12","doi-asserted-by":"crossref","unstructured":"Guthaus, M., Ringenberg, J., Ernst, D., Austin, T., Mudge, T., Brown, R.: MiBench: a free, commercially representative embedded benchmark suite. In: Proceedings of the Fourth Annual IEEE International Workshop on Workload Characterization. WWC-4. IEEE (2001). doi: 10.1109\/WWC.2001.990739","DOI":"10.1109\/WWC.2001.990739"},{"key":"77_CR13","doi-asserted-by":"crossref","unstructured":"Karaklaji\u0107, D., Schmidt, J.M., Verbauwhede, I.: Hardware Designer\u2019s Guide to Fault Attacks. In: IEEE Transactions on Very Large Scale Integration (VLSI) Systems (2013). doi: 10.1109\/TVLSI.2012.2231707","DOI":"10.1109\/TVLSI.2012.2231707"},{"key":"77_CR14","doi-asserted-by":"crossref","unstructured":"Medwed, M., Schmidt, J.M.: A generic fault countermeasure providing data and program flow integrity. In: 2008 Workshop on Fault Diagnosis and Tolerance in Cryptography. IEEE (2008). doi: 10.1109\/FDTC.2008.11","DOI":"10.1109\/FDTC.2008.11"},{"key":"77_CR15","doi-asserted-by":"crossref","unstructured":"Moro, N., Dehbaoui, A., Heydemann, K., Robisson, B., Encrenaz, E.: Electromagnetic fault injection: towards a fault model on a 32-bit microcontroller. In: 2013 Workshop on Fault Diagnosis and Tolerance in Cryptography. IEEE (2013). doi: 10.1109\/FDTC.2013.9","DOI":"10.1109\/FDTC.2013.9"},{"key":"77_CR16","doi-asserted-by":"crossref","unstructured":"Nguyen, M.H., Robisson, B., Agoyan, M., Drach, N.: Low-cost recovery for the code integrity protection in secure embedded processors. In: 2011 IEEE International Symposium on Hardware-Oriented Security and Trust. IEEE (2011). doi: 10.1109\/HST.2011.5955004","DOI":"10.1109\/HST.2011.5955004"},{"key":"77_CR17","doi-asserted-by":"crossref","unstructured":"Rauzy, P., Guilley, S.: A formal proof of countermeasures against fault injection attacks on CRT-RSA. J. Cryptogr. Eng. (2013). doi: 10.1007\/s13389-013-0065-3","DOI":"10.1007\/s13389-013-0065-3"},{"key":"77_CR18","doi-asserted-by":"crossref","unstructured":"Schmidt, J.M., Herbst, C.: A practical fault attack on square and multiply. In: 2008 Workshop on Fault Diagnosis and Tolerance in Cryptography. IEEE (2008). doi: 10.1109\/FDTC.2008.10","DOI":"10.1109\/FDTC.2008.10"},{"key":"77_CR19","doi-asserted-by":"crossref","unstructured":"Skorobogatov, S.: Local heating attacks on Flash memory devices. In: 2009 IEEE International Workshop on Hardware-Oriented Security and Trust, pp. 1\u20136. IEEE (2009). doi: 10.1109\/HST.2009.5225028","DOI":"10.1109\/HST.2009.5225028"},{"key":"77_CR20","doi-asserted-by":"crossref","unstructured":"Trichina, E., Korkikyan, R.: Multi fault laser attacks on protected CRT-RSA. In: 2010 Workshop on Fault Diagnosis and Tolerance in Cryptography. IEEE (2010). doi: 10.1109\/FDTC.2010.14","DOI":"10.1109\/FDTC.2010.14"},{"key":"77_CR21","doi-asserted-by":"crossref","unstructured":"Yiu, J.: The Definitive Guide To The ARM Cortex-M3. Elsevier Science, London (2009)","DOI":"10.1016\/B978-1-85617-963-8.00017-X"},{"key":"77_CR22","unstructured":"Zussa, L., Dutertre, J.M., Cl\u00e9di\u00e8re, J., Robisson, B., Tria, A.: Investigation of timing constraints violation as a fault injection means. In: DCIS. Avignon, France (2012)"}],"container-title":["Journal of Cryptographic Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s13389-014-0077-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s13389-014-0077-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s13389-014-0077-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T15:04:16Z","timestamp":1565190256000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s13389-014-0077-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2,19]]},"references-count":22,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,9]]}},"alternative-id":["77"],"URL":"https:\/\/doi.org\/10.1007\/s13389-014-0077-7","relation":{},"ISSN":["2190-8508","2190-8516"],"issn-type":[{"value":"2190-8508","type":"print"},{"value":"2190-8516","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,2,19]]}}}