{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:40:08Z","timestamp":1749318008617,"version":"3.41.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031937057","type":"print"},{"value":"9783031937064","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-93706-4_14","type":"book-chapter","created":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:22:37Z","timestamp":1749316957000},"page":"236-253","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Verification of\u00a0Composite Field Multipliers for\u00a0Information-Theoretically Secure Radio Communication in\u00a0Spacecraft Control"],"prefix":"10.1007","author":[{"given":"Sumio","family":"Morioka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Satoshi","family":"Obana","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maki","family":"Yoshida","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,6,8]]},"reference":[{"key":"14_CR1","unstructured":"Interstellar Technologies Inc. https:\/\/www.istellartech.com\/launch\/momo. Accessed 14 Mar 2025"},{"key":"14_CR2","unstructured":"Morioka, S., Inagawa, T.: (Invited paper) design requirements and implementation of avionics system on commercial space launch vehicles. J. Inst. Electron. Inf. Commun. Eng. 105(4), 1\u20138 (2022). https:\/\/www.journal.ieice.org\/bin\/pdf_link.php?fname=k105_4_275e. Accessed 14 Mar 2025"},{"key":"14_CR3","unstructured":"Interstellar Technologies Inc. https:\/\/www.istellartech.com\/launch\/zero. Accessed 14 Mar 2025"},{"key":"14_CR4","unstructured":"Morioka, S., et al.: (Invited talk) dense formation flying of multiple PicoSats for communication satellites and its technical challenges. In: Proceedings of IEICE 2024 Joint Conference on Satellite Communications (JC-SAT 2024), SAT2024-55 (2024)"},{"key":"14_CR5","unstructured":"Interstellar Technologies Inc. https:\/\/www.istellartech.com\/en\/satellite\/ourstars. Accessed 14 Mar 2025"},{"key":"14_CR6","doi-asserted-by":"publisher","first-page":"656","DOI":"10.1002\/j.1538-7305.1949.tb00928.x","volume":"28\u20134","author":"CE Shannon","year":"1949","unstructured":"Shannon, C.E.: Communication theory of secrecy systems. Bell Syst. Tech. J. 28\u20134, 656\u2013715 (1949)","journal-title":"Bell Syst. Tech. J."},{"key":"14_CR7","unstructured":"Morioka, S., Obana, S., Yoshida, M.: Flight demonstration results of information theoretically secure wireless communication on a sounding rocket MOMO. In: Proceedings of the 33rd International Symposium on Space Technology and Science (ISTS), Session J-2, 2022-j-06 (2022)"},{"key":"14_CR8","unstructured":"Morioka, S., Obana, S., Yoshida, M.: A fast information theoretically secure radio communication protocol based on GNSS positioning. In: Proceedings of the 34th Congress of the International Council of the Aeronautical Sciences (ICAS 2024) (2024)"},{"key":"14_CR9","doi-asserted-by":"publisher","unstructured":"Morioka, S., Obana, S., Yoshida, M.: Feasibility study with actual space rockets towards information theoretically secure radio communication. In: Arai, K. (eds.) Intelligent Computing. SAI 2024. Lecture Notes in Networks and Systems, vol. 1017. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-031-62277-9_32. Accessed 14 Mar 2025","DOI":"10.1007\/978-3-031-62277-9_32"},{"key":"14_CR10","first-page":"65","volume":"2","author":"B den Boer","year":"1993","unstructured":"den Boer, B.: A simple and key-economical unconditional authentication scheme. J. Comput. Secur. 2, 65\u201371 (1993)","journal-title":"J. Comput. Secur."},{"issue":"7","key":"14_CR11","doi-asserted-by":"publisher","first-page":"856","DOI":"10.1109\/12.508323","volume":"45","author":"C Paar","year":"1996","unstructured":"Paar, C.: A new architecture for a parallel finite field multiplier with low complexity based on composite fields. IEEE Trans. Comput. 45(7), 856\u2013861 (1996)","journal-title":"IEEE Trans. Comput."},{"issue":"10","key":"14_CR12","doi-asserted-by":"publisher","first-page":"1133","DOI":"10.1109\/12.888054","volume":"49","author":"S Oh","year":"2000","unstructured":"Oh, S., Kim, C.H., Lim, J., Cheon, D.H.: Efficient normal basis multipliers in composite fields. IEEE Trans. Comput. 49(10), 1133\u20131138 (2000)","journal-title":"IEEE Trans. Comput."},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Lee, C., Meher, P.K.: Efficient bit-parallel multipliers in composite fields. In: Proceedings of 2008 IEEE Asia-Pacific Services Computing Conference, pp. 686\u2013691 (2008)","DOI":"10.1109\/APSCC.2008.103"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Morioka, S., Satoh, A.: An optimized S-box circuit architecture for low power AES design. In: IACR Workshop on Cryptographic Hardware and Embedded Systems 2002 (CHES 2002). LNCS, vol. 2523, pp. 172\u2013186 (2002)","DOI":"10.1007\/3-540-36400-5_14"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Morioka, S., Katayama, Y., Yamane, T.: Towards efficient verification of arithmetic algorithms over Galois fields $$GF(2^m)$$. In: Proceedings of 13th Conference on Computer Aided Verification. LNCS, pp. 465\u2013477 (2001)","DOI":"10.1007\/3-540-44585-4_45"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Mukhopadhyay, D., Sengar, G., Chowdhury, R.D.: Hierarchical verification of Galois field circuits. IEEE Trans. Comput.-Aided Design Integr. Circuits Syst. 26(10), 1893\u20131898 (2007)","DOI":"10.1109\/TCAD.2007.895755"},{"issue":"1","key":"14_CR17","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/TIFS.2011.2157687","volume":"7","author":"N Homma","year":"2012","unstructured":"Homma, N., Saito, K., Aoki, T.: Formal approach to designing cryptographic processors based on $$ GF(2^m) $$ arithmetic circuits. IEEE Trans. Inf. Forensics Secur. 7(1), 3\u201313 (2012)","journal-title":"IEEE Trans. Inf. Forensics Secur."},{"issue":"10","key":"14_CR18","doi-asserted-by":"publisher","first-page":"2604","DOI":"10.1109\/TC.2013.131","volume":"63","author":"N Homma","year":"2014","unstructured":"Homma, N., Saito, K., Aoki, T.: Toward formal design of practical cryptographic hardware based on Galois field arithmetic. IEEE Trans. Comput. 63(10), 2604\u20132613 (2014)","journal-title":"IEEE Trans. Comput."},{"issue":"7","key":"14_CR19","doi-asserted-by":"publisher","first-page":"1396","DOI":"10.1587\/transfun.E100.A.1396","volume":"100","author":"R Ueno","year":"2017","unstructured":"Ueno, R., Homma, N., Aoki, T., Morioka, S.: Hierarchical formal verification combining algebraic transformation with PPRM expansion and its application to masked cryptographic processors. IEICE Trans. Fundam. 100(7), 1396\u20131408 (2017)","journal-title":"IEICE Trans. Fundam."},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Lv, J., Kalla, P., Enescu, F.: Verification of composite Galois field multipliers over $$GF((2^m)^n)$$ using computer algebra techniques. In: Proceedings of 2011 IEEE International Conference on High Level Design Validation and Test Workshop (HLDVT), pp. 136\u2013143 (2011)","DOI":"10.1109\/HLDVT.2011.6113989"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Lv, J., Kalla, P.: Formal verification of Galois field multipliers using computer algebra techniques. In: Proceedings of 2012 25th International Conference on VLSI Design (VLSID), pp. 76\u201379 (2012)","DOI":"10.1109\/VLSID.2012.102"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Lv, J., Kalla, P., Enescu, F.: Efficient Gr\u00f6bner basis reductions for formal verification of Galois field multipliers. In: Proceedings of 2012 Design, Automation & Test in Europe Conference & Exhibition (DATE), Dresden, Germany, pp. 899\u2013904 (2012)","DOI":"10.1109\/DATE.2012.6176625"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Su, T., Yasin, A., Yu, C., Ciesielski, M.: Computer algebraic approach to verification and debugging of Galois field multipliers. In: Proceedings of 2018 IEEE International Symposium on Circuits and Systems (ISCAS), Florence, Italy, pp. 1\u20135 (2018)","DOI":"10.1109\/ISCAS.2018.8351397"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Sasao, T.: Representations of logic functions using EXOR operators. In: Representations of Discrete Functions, pp. 29\u201354. Springer (1996)","DOI":"10.1007\/978-1-4613-1385-4_2"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Blake, I.F., Gao, X., Mullin, R.C., Vanstone, S.A., Yaghoobian, T.: Applications of Finite Fields. Kluwer Academic Publishers (1993)","DOI":"10.1007\/978-1-4757-2226-0"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"NIST: NIST SP 800-38D Recommendation for Block Cipher Modes of Operation: Galois\/Counter Mode (GCM) and GMAC. https:\/\/doi.org\/10.6028\/NIST.SP.800-38D. Accessed 14 Mar 2025","DOI":"10.6028\/NIST.SP.800-38d"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Von Zur Gathen, J., Panario, D.: Factoring polynomials over finite fields: a survey. J. Symb. Comput. 31, 3\u201317 (2001)","DOI":"10.1006\/jsco.1999.1002"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Kebshull, U., Rosenstiel, W.: Efficient graph-based computation and manipulation of functional decision diagrams. In: European Design Automation Conference 1993, pp. 278\u2013282 (1993)","DOI":"10.1109\/EDAC.1993.386463"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-93706-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:22:42Z","timestamp":1749316962000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-93706-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031937057","9783031937064"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-93706-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"8 June 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hampton Roads, VA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}