{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T17:50:23Z","timestamp":1649094623959},"reference-count":26,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"8","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. &amp; Syst."],"published-print":{"date-parts":[[2021,8,1]]},"DOI":"10.1587\/transinf.2020lop0004","type":"journal-article","created":{"date-parts":[[2021,7,31]],"date-time":"2021-07-31T22:16:34Z","timestamp":1627769794000},"page":"1083-1091","source":"Crossref","is-referenced-by-count":0,"title":["An Algebraic Approach to Verifying Galois-Field Arithmetic Circuits with Multiple-Valued Characteristics"],"prefix":"10.1587","volume":"E104.D","author":[{"given":"Akira","family":"ITO","sequence":"first","affiliation":[{"name":"Tohoku University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rei","family":"UENO","sequence":"additional","affiliation":[{"name":"Tohoku University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naofumi","family":"HOMMA","sequence":"additional","affiliation":[{"name":"Tohoku University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"532","reference":[{"key":"1","doi-asserted-by":"publisher","unstructured":"[1] E. Savas and C.K. Koc, \u201cFinite field arithmetic for cryptography,\u201d IEEE Circuits and Systems Magazine, vol.10, no.2, pp.40-56, Secondquarter 2010. 10.1109\/MCAS.2010.936785","DOI":"10.1109\/MCAS.2010.936785"},{"key":"2","doi-asserted-by":"publisher","unstructured":"[2] I. Duursma and H.S. Lee, \u201cTate pairing implementation for hyperelliptic curves <i>y<\/i><sup>2<\/sup>=<i>x<sup>p<\/sup><\/i>-<i>x<\/i>+<i>d<\/i>,\u201d Advances in Cryptology-ASIACRYPT 2003, ed. C.S. Laih, Lect. Notes Comput. Sci., vol.2894, pp.111-123, Springer, Berlin, Heidelberg, 2003. 10.1007\/978-3-540-40061-5_7","DOI":"10.1007\/978-3-540-40061-5_7"},{"key":"3","doi-asserted-by":"crossref","unstructured":"[3] D.J. Bernstein, N. Duif, T. Lange, P. Schwabe, and B.Y. Yang, \u201cHigh-speed high-security signatures,\u201d J. Cryptographic Engineering, vol.2, no.2, pp.77-89, Sept. 2012. 10.1007\/s13389-012-0027-1","DOI":"10.1007\/s13389-012-0027-1"},{"key":"4","doi-asserted-by":"crossref","unstructured":"[4] D. Boneh, B. Lynn, and H. Shacham, \u201cShort Signatures from the Weil Pairing,\u201d J. Cryptology, vol.17, no.4, pp.297-319, Sept. 2004. 10.1007\/s00145-004-0314-9","DOI":"10.1007\/s00145-004-0314-9"},{"key":"5","doi-asserted-by":"publisher","unstructured":"[6] E. Lee, H.S. Lee, and Y. Lee, \u201cEta pairing computation on general divisors over hyperelliptic curves <i>y<\/i><sup>2<\/sup>=<i>x<sup>p<\/sup><\/i>-<i>x<\/i>+<i>d<\/i>,\u201d J. Symbolic Computation, vol.43, no.6, pp.452-474, June 2008. 10.1016\/j.jsc.2007.07.010","DOI":"10.1016\/j.jsc.2007.07.010"},{"key":"6","doi-asserted-by":"publisher","unstructured":"[7] J. Lv, P. Kalla, and F. Enescu, \u201cEfficient Gr\u00f6bner Basis Reductions for Formal Verification of Galois Field Arithmetic Circuits,\u201d IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., vol.32, no.9, pp.1409-1420, Sept. 2013. 10.1109\/TCAD.2013.2259540","DOI":"10.1109\/TCAD.2013.2259540"},{"key":"7","doi-asserted-by":"crossref","unstructured":"[8] R.E. Bryant and Y.A. Chen, \u201cVerification of Arithmetic Circuits with Binary Moment Diagrams,\u201d Design Automation Conference, pp.535-541, Jan. 1995. 10.1145\/217474.217583","DOI":"10.1145\/217474.217583"},{"key":"8","doi-asserted-by":"publisher","unstructured":"[9] R. Drechsler and D. Sieling, \u201cBinary decision diagrams in theory and practice,\u201d International J. Software Tools for Technology Transfer, vol.3, no.2, pp.112-136, May 2001. 10.1007\/s100090100056","DOI":"10.1007\/s100090100056"},{"key":"9","doi-asserted-by":"publisher","unstructured":"[10] J. Jain, J. Bitner, M.S. Abadir, J.A. Abraham, and D.S. Fussell, \u201cIndexed BDDs: Algorithmic advances in techniques to represent and verify Boolean functions,\u201d IEEE Trans. Comput., vol.46, no.11, pp.1230-1245, Nov. 1997. 10.1109\/12.644298","DOI":"10.1109\/12.644298"},{"key":"10","doi-asserted-by":"publisher","unstructured":"[11] B. Bollig, M. Sauerhoff, D. Sieling, and I. Wegener, \u201cHierarchy theorems for kOBDDs and kIBDDs,\u201d Theoretical Computer Science, vol.205, no.1, pp.45-60, Sept. 1998. 10.1016\/S0304-3975(97)00034-0","DOI":"10.1016\/S0304-3975(97)00034-0"},{"key":"11","doi-asserted-by":"crossref","unstructured":"[12] B. Becker, R. Drechsler, and R. Werchner, \u201cOn the relation between BDDs and FDDs,\u201d LATIN &apos;95: Theoretical Informatics, ed. R. Baeza-Yates, E. Goles, and P.V. Poblete, Lect. Notes Comput. Sci., vol.911, pp.72-83, Springer, Berlin, Heidelberg, 1995. 10.1007\/3-540-59175-3_82","DOI":"10.1007\/3-540-59175-3_82"},{"key":"12","doi-asserted-by":"publisher","unstructured":"[13] U. Gupta, P. Kalla, and V. Rao, \u201cBoolean Gr\u00f6bner Basis Reductions on Finite Field Datapath Circuits Using the Unate Cube Set Algebra,\u201d IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., vol.38, no.3, pp.576-588, March 2019. 10.1109\/TCAD.2018.2818726","DOI":"10.1109\/TCAD.2018.2818726"},{"key":"13","doi-asserted-by":"publisher","unstructured":"[14] A. Ito, R. Ueno, and N. Homma, \u201cEfficient Formal Verification of Galois-Field Arithmetic Circuits Using ZDD Representation of Boolean Polynomials,\u201d IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., in press. 10.1109\/TCAD.2021.3059924","DOI":"10.1109\/TCAD.2021.3059924"},{"key":"14","doi-asserted-by":"publisher","unstructured":"[15] N. Homma, K. Saito, and T. Aoki, \u201cA formal approach to designing cryptographic processors based on <i>gf<\/i>(2<i><sup>m<\/sup><\/i>) arithmetic circuits,\u201d IEEE Trans. Inf. Forensics Security, vol.7, no.1, pp.3-13, Feb. 2012. 10.1109\/TIFS.2011.2157687","DOI":"10.1109\/TIFS.2011.2157687"},{"key":"15","doi-asserted-by":"crossref","unstructured":"[16] A. Ito, R. Ueno, and N. Homma, \u201cEffective Formal Verification for Galois-field Arithmetic Circuits with Multiple-Valued Characteristics,\u201d 2020 IEEE 50th Int. Symp. Multiple-Valued Logic (ISMVL), pp.46-51, Nov. 2020. 10.1109\/ISMVL49045.2020.00-31","DOI":"10.1109\/ISMVL49045.2020.00-31"},{"key":"16","doi-asserted-by":"publisher","unstructured":"[17] N. Homma, K. Saito, and T. Aoki, \u201cToward Formal Design of Practical Cryptographic Hardware Based on Galois Field Arithmetic,\u201d IEEE Trans. Comput., vol.63, no.10, pp.2604-2613, Oct. 2014. 10.1109\/TC.2013.131","DOI":"10.1109\/TC.2013.131"},{"key":"17","doi-asserted-by":"publisher","unstructured":"[18] R. Ueno, N. Homma, Y. Sugawara, and T. Aoki, \u201cFormal Approach for Verifying Galois Field Arithmetic Circuits of Higher Degrees,\u201d IEEE Trans. Comput., vol.66, no.3, pp.431-442, March 2017. 10.1109\/TC.2016.2603979","DOI":"10.1109\/TC.2016.2603979"},{"key":"18","doi-asserted-by":"publisher","unstructured":"[19] R. Ueno, N. Homma, and T. Aoki, \u201cAutomatic Generation System for Multiple-Valued Galois-Field Parallel Multipliers,\u201d IEICE Trans. Inf. &amp; Syst., vol.E100-D, no.8, pp.1603-1610, Aug. 2017. 10.1587\/transinf.2016LOP0010","DOI":"10.1587\/transinf.2016LOP0010"},{"key":"19","doi-asserted-by":"publisher","unstructured":"[20] C. Yu and M. Ciesielski, \u201cFormal Analysis of Galois Field Arithmetic Circuits-Parallel Verification and Reverse Engineering,\u201d IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., vol.38, no.2, pp.354-365, Feb. 2019. 10.1109\/TCAD.2018.2808457","DOI":"10.1109\/TCAD.2018.2808457"},{"key":"20","doi-asserted-by":"crossref","unstructured":"[21] S.i. Minato, \u201cZero-suppressed BDDs for set manipulation in combinatorial problems,\u201d Proc. 30th International Design Automation Conference, pp.272-277, July 1993. 10.1145\/157485.164890","DOI":"10.1145\/157485.164890"},{"key":"21","doi-asserted-by":"publisher","unstructured":"[22] S.i. Minato, \u201cZero-suppressed BDDs and their applications,\u201d International J. Software Tools for Technology Transfer, vol.3, no.2, pp.156-170, May 2001. 10.1007\/s100090100038","DOI":"10.1007\/s100090100038"},{"key":"22","unstructured":"[23] D. Miller and R. Drechsler, \u201cOn the construction of multiple-valued decision diagrams,\u201d Proceedings 32nd IEEE Int. Symp. Multiple-Valued Logic, pp.245-253, May 2002. 10.1109\/ISMVL.2002.1011095"},{"key":"23","unstructured":"[24] A. Jabir and D. Pradhan, \u201cMODD: A new decision diagram and representation for multiple output binary functions,\u201d Automation and Test in Europe Conference and Exhibition Proceedings Design, pp.1388-1389 vol.2, Feb. 2004. 10.1109\/DATE.2004.1269101"},{"key":"24","unstructured":"[25] R. Stankovic, \u201cFunctional decision diagrams for multiple-valued functions,\u201d Proceedings 25th Int. Symp. Multiple-Valued Logic, pp.284-289, May 1995. 10.1109\/ISMVL.1995.513544"},{"key":"25","doi-asserted-by":"publisher","unstructured":"[26] T. Pruss, P. Kalla, and F. Enescu, \u201cEfficient Symbolic Computation for Word-Level Abstraction From Combinational Circuits for Verification Over Finite Fields,\u201d IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., vol.35, no.7, pp.1206-1218, July 2016. 10.1109\/TCAD.2015.2501301","DOI":"10.1109\/TCAD.2015.2501301"},{"key":"26","doi-asserted-by":"crossref","unstructured":"[27] R. Bryant and Y.a. Chen, \u201cVerification of Arithmetic Functions with Binary Moment Diagrams,\u201d Technical Report CMUCS, May 1994.","DOI":"10.21236\/ADA281028"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E104.D\/8\/E104.D_2020LOP0004\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,7]],"date-time":"2021-08-07T06:25:13Z","timestamp":1628317513000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E104.D\/8\/E104.D_2020LOP0004\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,1]]},"references-count":26,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2021]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2020lop0004","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"value":"0916-8532","type":"print"},{"value":"1745-1361","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,1]]},"article-number":"2020LOP0004"}}