{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T01:24:51Z","timestamp":1783905891035,"version":"3.55.0"},"reference-count":8,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2019,4,1]],"date-time":"2019-04-01T00:00:00Z","timestamp":1554076800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,4,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>\n                    In this article we formalize in Mizar [1], [2] the maximum number of steps taken by some number theoretical algorithms, \u201cright\u2013to\u2013left binary algorithm\u201d for modular exponentiation and \u201cEuclidean algorithm\u201d [5]. For any natural numbers\n                    <jats:italic>a<\/jats:italic>\n                    ,\n                    <jats:italic>b<\/jats:italic>\n                    ,\n                    <jats:italic>n<\/jats:italic>\n                    , \u201cright\u2013to\u2013left binary algorithm\u201d can calculate the natural number, see (Def. 2), Algo\n                    <jats:sub>BPow<\/jats:sub>\n                    (\n                    <jats:italic>a, n, m<\/jats:italic>\n                    ) :=\n                    <jats:italic>\n                      a\n                      <jats:sup>b<\/jats:sup>\n                    <\/jats:italic>\n                    mod\n                    <jats:italic>n<\/jats:italic>\n                    and for any integers\n                    <jats:italic>a<\/jats:italic>\n                    ,\n                    <jats:italic>b<\/jats:italic>\n                    , \u201cEuclidean algorithm\u201d can calculate the non negative integer gcd(\n                    <jats:italic>a, b<\/jats:italic>\n                    ). We have not formalized computational complexity of algorithms yet, though we had already formalize the \u201cEuclidean algorithm\u201d in [7].\n                  <\/jats:p>\n                  <jats:p>\n                    For \u201cright-to-left binary algorithm\u201d, we formalize the theorem, which says that the required number of the modular squares and modular products in this algorithms are \u230a1+log\n                    <jats:sub>2<\/jats:sub>\n                    <jats:italic>n<\/jats:italic>\n                    \u230b and for \u201cEuclidean algorithm\u201d, we formalize the Lam\u00e9\u2019s theorem [6], which says the required number of the divisions in this algorithm is at most 5 log\n                    <jats:sub>10<\/jats:sub>\n                    min(\n                    <jats:italic>|a|, |b|<\/jats:italic>\n                    ). Our aim is to support the implementation of number theoretic tools and evaluating computational complexities of algorithms to prove the security of cryptographic systems.\n                  <\/jats:p>","DOI":"10.2478\/forma-2019-0009","type":"journal-article","created":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T05:34:02Z","timestamp":1558071242000},"page":"87-91","source":"Crossref","is-referenced-by-count":0,"title":["Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm"],"prefix":"10.2478","volume":"27","author":[{"given":"Hiroyuki","family":"Okazaki","sequence":"first","affiliation":[{"name":"Shinshu University , Nagano , Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Koh-ichi","family":"Nagao","sequence":"additional","affiliation":[{"name":"Kanto Gakuin University , Kanagawa , Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yuichi","family":"Futa","sequence":"additional","affiliation":[{"name":"Tokyo University of Technology , Tokyo , Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"374","published-online":{"date-parts":[[2019,5,16]]},"reference":[{"key":"2026071214315439427_j_forma-2019-0009_ref_001_w2aab3b7b8b1b6b1ab1ab1Aa","doi-asserted-by":"crossref","unstructured":"[1] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, Karol P\u0105k, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261\u2013279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007\/978-3-319-20615-8_17.10.1007\/978-3-319-20615-8_17","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"2026071214315439427_j_forma-2019-0009_ref_002_w2aab3b7b8b1b6b1ab1ab2Aa","doi-asserted-by":"crossref","unstructured":"[2] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, and Karol P\u0105k. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9\u201332, 2018. doi:10.1007\/s10817-017-9440-6.10.1007\/s10817-017-9440-6604425130069070","DOI":"10.1007\/s10817-017-9440-6"},{"key":"2026071214315439427_j_forma-2019-0009_ref_003_w2aab3b7b8b1b6b1ab1ab3Aa","unstructured":"[3] Yoshinori Fujisawa, Yasushi Fuwa, and Hidetaka Shimizu. Euler\u2019s Theorem and small Fermat\u2019s Theorem. Formalized Mathematics, 7(1):123\u2013126, 1998."},{"key":"2026071214315439427_j_forma-2019-0009_ref_004_w2aab3b7b8b1b6b1ab1ab4Aa","unstructured":"[4] Magdalena Jastrz\u0119bska and Adam Grabowski. Some properties of Fibonacci numbers. Formalized Mathematics, 12(3):307\u2013313, 2004."},{"key":"2026071214315439427_j_forma-2019-0009_ref_005_w2aab3b7b8b1b6b1ab1ab5Aa","unstructured":"[5] Donald E. Knuth. Art of Computer Programming. Volume 2: Seminumerical Algorithms, 3rd Edition, Addison-Wesley Professional, 1997."},{"key":"2026071214315439427_j_forma-2019-0009_ref_006_w2aab3b7b8b1b6b1ab1ab6Aa","unstructured":"[6] Gabriel Lam\u00e9. Note sur la limite du nombre des divisions dans la recherche du plus grand commun diviseur entre deux nombres entiers. Comptes Rendus Acad. Sci., 19:867\u2013870, 1844."},{"key":"2026071214315439427_j_forma-2019-0009_ref_007_w2aab3b7b8b1b6b1ab1ab7Aa","doi-asserted-by":"crossref","unstructured":"[7] Hiroyuki Okazaki, Yosiki Aoki, and Yasunari Shidama. Extended Euclidean algorithm and CRT algorithm. Formalized Mathematics, 20(2):175\u2013179, 2012. doi:10.2478\/v10037-012-0020-2.10.2478\/v10037-012-0020-2","DOI":"10.2478\/v10037-012-0020-2"},{"key":"2026071214315439427_j_forma-2019-0009_ref_008_w2aab3b7b8b1b6b1ab1ab8Aa","doi-asserted-by":"crossref","unstructured":"[8] Marco Riccardi. Pocklington\u2019s theorem and Bertrand\u2019s postulate. Formalized Mathematics, 14(2):47\u201352, 2006. doi:10.2478\/v10037-006-0007-y.10.2478\/v10037-006-0007-y","DOI":"10.2478\/v10037-006-0007-y"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/27\/1\/article-p87.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2019-0009","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T00:58:04Z","timestamp":1783904284000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2019-0009"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4,1]]},"references-count":8,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2019,5,16]]},"published-print":{"date-parts":[[2019,4,1]]}},"alternative-id":["10.2478\/forma-2019-0009"],"URL":"https:\/\/doi.org\/10.2478\/forma-2019-0009","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2019,4,1]]}}}