default search action
Hiroyuki Okazaki
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Journal Articles
- 2024
- [j57]Takehiko Mieno, Hiroyuki Okazaki, Kenichi Arai, Yuichi Futa:
How to Formalize Loop Iterations in Cryptographic Protocols Using ProVerif. IEEE Access 12: 31605-31625 (2024) - 2023
- [j56]Hiroyuki Okazaki:
On the Formalization of Gram-Schmidt Process for Orthonormalizing a Set of Vectors. Formaliz. Math. 31(1): 53-57 (2023) - 2022
- [j55]Hiroyuki Okazaki:
Formalization of Orthogonal Decomposition for Hilbert Spaces. Formaliz. Math. 30(4): 295-299 (2022) - 2021
- [j54]Kazuhisa Nakasho, Hiroyuki Okazaki, Yasunari Shidama:
Real Vector Space and Related NotionsThis study was supported in part by JSPS KAKENHI Grant Numbers 17K00182 and 20K19863. Formaliz. Math. 29(3): 117-127 (2021) - [j53]Kazuhisa Nakasho, Hiroyuki Okazaki, Yasunari Shidama:
Finite Dimensional Real Normed Spaces are Proper Metric Spaces. Formaliz. Math. 29(4): 175-184 (2021) - [j52]Hiroyuki Okazaki, Kazuhisa Nakasho:
The 3-Fold Product Space of Real Normed Spaces and its Properties. Formaliz. Math. 29(4): 241-248 (2021) - 2019
- [j51]Hiroyuki Okazaki, Koh-ichi Nagao, Yuichi Futa:
Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm. Formaliz. Math. 27(1): 87-91 (2019) - [j50]Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama:
Operations of Points on Elliptic Curve in Affine Coordinates. Formaliz. Math. 27(3): 315-320 (2019) - 2018
- [j49]Hiroyuki Okazaki:
Binary Representation of Natural Numbers. Formaliz. Math. 26(3): 223-229 (2018) - 2016
- [j48]Kazuhisa Nakasho, Hiroshi Yamazaki, Hiroyuki Okazaki, Yasunari Shidama:
Conservation Rules of Direct Sum Decomposition of Groups. Formaliz. Math. 24(1): 81-94 (2016) - 2015
- [j47]Kazuhisa Nakasho, Hiroshi Yamazaki, Hiroyuki Okazaki, Yasunari Shidama:
Definition and Properties of Direct Sum Decomposition of Groups1. Formaliz. Math. 23(1): 15-27 (2015) - [j46]Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama:
Matrix of ℤ-module1. Formaliz. Math. 23(1): 29-49 (2015) - [j45]Kazuhisa Nakasho, Hiroyuki Okazaki, Hiroshi Yamazaki, Yasunari Shidama:
Equivalent Expressions of Direct Sum Decomposition of Groups1. Formaliz. Math. 23(1): 67-73 (2015) - [j44]Hiroyuki Okazaki, Yuichi Futa:
Polynomially Bounded Sequences and Polynomial Sequences. Formaliz. Math. 23(3): 205-213 (2015) - [j43]Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama:
Torsion Part of ℤ-module. Formaliz. Math. 23(4): 297-307 (2015) - [j42]Hiroyuki Okazaki:
Algebra of Polynomially Bounded Sequences and Negligible Functions. Formaliz. Math. 23(4): 371-378 (2015) - 2014
- [j41]Kazuhisa Nakasho, Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama:
Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module. Formaliz. Math. 22(3): 189-198 (2014) - [j40]Kenichi Arai, Ken Wakabayashi, Hiroyuki Okazaki:
Difference of Function on Vector Space over F. Formaliz. Math. 22(3): 269-275 (2014) - [j39]Yuichi Futa, Hiroyuki Okazaki, Kazuhisa Nakasho, Yasunari Shidama:
Torsion Z-module and Torsion-free Z-module. Formaliz. Math. 22(4): 277-289 (2014) - 2013
- [j38]Hiroyuki Okazaki, Yuichi Futa, Yasunari Shidama:
Formal definition of probability on finite and discrete sample space for proving security of cryptographic systems using Mizar. Artif. Intell. Res. 2(4): 37-48 (2013) - [j37]Katuhiko Kanazashi, Hiroyuki Okazaki, Yasunari Shidama:
The Ck Space. Formaliz. Math. 21(1): 25-31 (2013) - [j36]Hiroyuki Okazaki, Yasunari Shidama:
Random Variables and Product of Probability Spaces. Formaliz. Math. 21(1): 33-39 (2013) - [j35]Hiroyuki Okazaki, Hiroshi Yamazaki, Yasunari Shidama:
Isomorphisms of Direct Products of Finite Commutative Groups. Formaliz. Math. 21(1): 65-74 (2013) - [j34]Kenichi Arai, Hiroyuki Okazaki:
N-Dimensional Binary Vector Spaces. Formaliz. Math. 21(2): 75-81 (2013) - [j33]Yuichi Futa, Hiroyuki Okazaki, Daichi Mizushima, Yasunari Shidama:
Gaussian Integers. Formaliz. Math. 21(2): 115-125 (2013) - [j32]Hiroyuki Okazaki, Yuichi Futa, Yasunari Shidama:
Constructing Binary Huffman Tree. Formaliz. Math. 21(2): 133-143 (2013) - [j31]Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama:
Double Sequences and Limits. Formaliz. Math. 21(3): 163-170 (2013) - [j30]Kenichi Arai, Hiroyuki Okazaki:
Formalization of the Advanced Encryption Standard. Part I. Formaliz. Math. 21(3): 171-184 (2013) - [j29]Hiroshi Yamazaki, Hiroyuki Okazaki, Kazuhisa Nakasho, Yasunari Shidama:
Isomorphisms of Direct Products of Cyclic Groups of Prime Power Order. Formaliz. Math. 21(3): 207-211 (2013) - [j28]Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama:
Submodule of free Z-module. Formaliz. Math. 21(4): 273-282 (2013) - [j27]Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama:
Formalization of Definitions and Theorems Related to an Elliptic Curve Over a Finite Prime Field by Using Mizar. J. Autom. Reason. 50(2): 161-172 (2013) - 2012
- [j26]Katuhiko Kanazashi, Hiroyuki Okazaki, Yasunari Shidama:
Functional Space C(ω), C0(ω). Formaliz. Math. 20(1): 15-22 (2012) - [j25]Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama:
Z-modules. Formaliz. Math. 20(1): 47-59 (2012) - [j24]Yuichi Futa, Hiroyuki Okazaki, Daichi Mizushima, Yasunari Shidama:
Operations of Points on Elliptic Curve in Projective Coordinates. Formaliz. Math. 20(1): 87-95 (2012) - [j23]Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama:
Higher-Order Partial Differentiation. Formaliz. Math. 20(2): 113-124 (2012) - [j22]Hiroyuki Okazaki, Yasunari Shidama:
Formalization of the Data Encryption Standard. Formaliz. Math. 20(2): 125-146 (2012) - [j21]Hiroyuki Okazaki, Yosiki Aoki, Yasunari Shidama:
Extended Euclidean Algorithm and CRT Algorithm. Formaliz. Math. 20(2): 175-179 (2012) - [j20]Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama:
Quotient Module of Z-module. Formaliz. Math. 20(3): 205-214 (2012) - [j19]Hiroyuki Okazaki:
Posterior Probability on Finite Set. Formaliz. Math. 20(4): 257-263 (2012) - [j18]Hideki Sakurai, Hiroyuki Okazaki, Yasunari Shidama:
Banach's Continuous Inverse Theorem and Closed Graph Theorem. Formaliz. Math. 20(4): 271-274 (2012) - [j17]Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama:
Free ℤ-module. Formaliz. Math. 20(4): 275-280 (2012) - [j16]Kenichi Arai, Hiroyuki Okazaki, Yasunari Shidama:
Isomorphisms of Direct Products of Finite Cyclic Groups. Formaliz. Math. 20(4): 343-347 (2012) - 2011
- [j15]Hiroyuki Okazaki, Kenichi Arai, Yasunari Shidama:
Normal Subgroup of Product of Groups. Formaliz. Math. 19(1): 23-26 (2011) - [j14]Hiroyuki Okazaki, Noboru Endou, Yasunari Shidama:
More on Continuous Functions on Normed Linear Spaces. Formaliz. Math. 19(1): 45-49 (2011) - [j13]Hiroyuki Okazaki, Noboru Endou, Yasunari Shidama:
Cartesian Products of Family of Real Linear Spaces. Formaliz. Math. 19(1): 51-59 (2011) - [j12]Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama:
Formalization of Integral Linear Space. Formaliz. Math. 19(1): 61-64 (2011) - [j11]Hiroyuki Okazaki, Noboru Endou, Keiko Narita, Yasunari Shidama:
Differentiable Functions into Real Normed Spaces. Formaliz. Math. 19(2): 69-72 (2011) - [j10]Katuhiko Kanazashi, Hiroyuki Okazaki, Yasunari Shidama:
Banach Algebra of Bounded Complex-Valued Functionals. Formaliz. Math. 19(2): 121-126 (2011) - [j9]Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama:
Set of Points on Elliptic Curve in Projective Coordinates. Formaliz. Math. 19(3): 131-138 (2011) - 2010
- [j8]Hiroyuki Okazaki, Yasunari Shidama:
Probability Measure on Discrete Spaces and Algebra of Real-Valued Random Variables. Formaliz. Math. 18(1-4): 213-217 (2010) - 2009
- [j7]Hiroyuki Okazaki, Yasunari Shidama:
Probability on Finite Set and Real-Valued Random Variables. Formaliz. Math. 17(1-4): 129-136 (2009) - [j6]Kenichi Arai, Hiroyuki Okazaki:
Properties of Primes and Multiplicative Group of a Field. Formaliz. Math. 17(1-4): 151-155 (2009) - [j5]Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama:
Hopf Extension Theorem of Measure. Formaliz. Math. 17(1-4): 157-162 (2009) - [j4]Hiroyuki Okazaki:
Probability on Finite and Discrete Set and Uniform Distribution. Formaliz. Math. 17(1-4): 173-178 (2009) - 2008
- [j3]Hiroyuki Okazaki, Yasunari Shidama:
Uniqueness of Factoring an Integer and Multiplicative Group Z/pZ*. Formaliz. Math. 16(1-4): 103-107 (2008) - 1998
- [j2]Masayoshi Ejiri, Jong-Tae Park, Hiroyuki Okazaki, James Won-Ki Hong:
Managing the New Telecommunications Paradigms: A Report on APNOMS'98. J. Netw. Syst. Manag. 6(4): 497-500 (1998) - 1993
- [j1]Hideki Sakauchi, Yasuyo Okanoue, Hiroyuki Okazaki, Satoshi Hasegawa:
Distributed Self-Healing Control in SONET. J. Netw. Syst. Manag. 1(2): 123-141 (1993)
Conference and Workshop Papers
- 2021
- [c11]Ryo Tokuyama, Yuichi Futa, Hikofumi Suzuki, Hiroyuki Okazaki:
Virtual Environment for Analysis and Evaluation of DDoS Attacks. AINA (3) 2021: 459-468 - 2020
- [c10]Takehiko Mieno, Togo Yoshimura, Hiroyuki Okazaki, Yuichi Futa, Kenichi Arai:
Formal Verification of Merkle-Damgård Construction in ProVerif. ISITA 2020: 602-606 - 2018
- [c9]Hiroyuki Okazaki, Yuichi Futa, Kenichi Arai:
Suitable Symbolic Models for Cryptographic Verification of Secure Protocols in ProVerif. ISITA 2018: 326-330 - 2016
- [c8]Hiroyuki Okazaki, Yuichi Futa:
Formalization of Polynomially Bounded and Negligible Functions Using the Computer-Aided Proof-Checking System Mizar. FM4M/MathUI/ThEdu/DP/WIP@CIKM 2016: 117-131 - [c7]Hiroyuki Okazaki:
Formalization of statistical indistinguishability of probability distribution ensembles in Mizar. ISITA 2016: 517-521 - [c6]Hiroshi Yamaguchi, Shigeo Tsujii, Hiroyuki Okazaki, Yasunari Shidama:
Privacy Preserving Logic Formula Calculation in Cloud. ICSC 2016: 329-332 - 2015
- [c5]Hiroyuki Okazaki, Hiroki Matsumoto, Yoshiki Shibata, Shinichi Motomura, Naoyuki Masada:
Application to Women's Healthcare of Health Management System Using a Tablet Phone. BIH 2015: 262-271 - 2012
- [c4]Yuichi Futa, Daichi Mizushima, Hiroyuki Okazaki:
Formalization of Gaussian integers, Gaussian rational numbers, and their algebraic structures with Mizar. ISITA 2012: 591-595 - 2010
- [c3]Kenichi Arai, Nobuaki Kondo, Hiroyuki Okazaki:
Formalization of Probability and Random Sampling on a Finite and Discrete Sample Space Using the Mizar Proof Checker. FCS 2010: 81-86 - 2007
- [c2]Hernán E. Aguirre, Hiroyuki Okazaki, Yasushi Fuwa:
An evolutionary multiobjective approach to design highly non-linear Boolean functions. GECCO 2007: 749-756 - 1996
- [c1]T. Kawagoe, H. Kawakami, K. Soga, K. Tanaka, Hiroyuki Okazaki, Satoshi Hasegawa:
On the design and an implementation of broadband access management systems. NOMS 1996: 382-391
Informal and Other Publications
- 2005
- [i1]Hiroyuki Okazaki, Ryuichi Sakai, Masao Kasahara:
Meta Ring Signature. IACR Cryptol. ePrint Arch. 2005: 310 (2005)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from , , and to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 22:12 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint