Hiroyuki Okazaki

72 papers A 1B 1C 5Journal 60Unranked 5

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	Formalization of Separable Version of Banach-Alaoglu Theorem. Formaliz. Math. Hiroyuki Okazaki, Takehiko Mieno
2024	C	`conf`	Formal Security Verification for Searchable Symmetric Encryption Using ProVerif. ISITA Takehiko Mieno, Hiroyuki Okazaki, Kenichi Arai, Yuichi Futa, Hiroaki Yamamoto
2024	J	`jnl`	Formalization of Orthogonal Complements of Normed Spaces. Formaliz. Math. Hiroyuki Okazaki
2024	J	`jnl`	How to Formalize Loop Iterations in Cryptographic Protocols Using ProVerif. IEEE Access Takehiko Mieno, Hiroyuki Okazaki, Kenichi Arai, Yuichi Futa
2023	J	`jnl`	On the Formalization of Gram-Schmidt Process for Orthonormalizing a Set of Vectors. Formaliz. Math. Hiroyuki Okazaki
2022	J	`jnl`	Formalization of Orthogonal Decomposition for Hilbert Spaces. Formaliz. Math. Hiroyuki Okazaki
2021	J	`jnl`	Finite Dimensional Real Normed Spaces are Proper Metric Spaces. Formaliz. Math. Kazuhisa Nakasho, Hiroyuki Okazaki, Yasunari Shidama
2021	J	`jnl`	Real Vector Space and Related NotionsThis study was supported in part by JSPS KAKENHI Grant Numbers 17K00182 and 20K19863. Formaliz. Math. Kazuhisa Nakasho, Hiroyuki Okazaki, Yasunari Shidama
2021	J	`jnl`	The 3-Fold Product Space of Real Normed Spaces and its Properties. Formaliz. Math. Hiroyuki Okazaki, Kazuhisa Nakasho
2021	—	`conf`	Virtual Environment for Analysis and Evaluation of DDoS Attacks. AINA (3) Ryo Tokuyama, Yuichi Futa, Hikofumi Suzuki, Hiroyuki Okazaki
2020	C	`conf`	Formal Verification of Merkle-Damgård Construction in ProVerif. ISITA Takehiko Mieno, Togo Yoshimura, Hiroyuki Okazaki, Yuichi Futa, Kenichi Arai
2019	J	`jnl`	Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm. Formaliz. Math. Hiroyuki Okazaki, Koh-ichi Nagao, Yuichi Futa
2019	J	`jnl`	Operations of Points on Elliptic Curve in Affine Coordinates. Formaliz. Math. Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
2018	J	`jnl`	Binary Representation of Natural Numbers. Formaliz. Math. Hiroyuki Okazaki
2018	C	`conf`	Suitable Symbolic Models for Cryptographic Verification of Secure Protocols in ProVerif. ISITA Hiroyuki Okazaki, Yuichi Futa, Kenichi Arai
2016	J	`jnl`	Conservation Rules of Direct Sum Decomposition of Groups. Formaliz. Math. Kazuhisa Nakasho, Hiroshi Yamazaki, Hiroyuki Okazaki, Yasunari Shidama
2016	—	`conf`	Formalization of Polynomially Bounded and Negligible Functions Using the Computer-Aided Proof-Checking System Mizar. FM4M/MathUI/ThEdu/DP/WIP@CIKM Hiroyuki Okazaki, Yuichi Futa
2016	C	`conf`	Formalization of statistical indistinguishability of probability distribution ensembles in Mizar. ISITA Hiroyuki Okazaki
2016	—	`conf`	Privacy Preserving Logic Formula Calculation in Cloud. ICSC Hiroshi Yamaguchi, Shigeo Tsujii, Hiroyuki Okazaki, Yasunari Shidama
2015	J	`jnl`	Algebra of Polynomially Bounded Sequences and Negligible Functions. Formaliz. Math. Hiroyuki Okazaki
2015	—	`conf`	Application to Women's Healthcare of Health Management System Using a Tablet Phone. BIH Hiroyuki Okazaki, Hiroki Matsumoto, Yoshiki Shibata, Shinichi Motomura, Naoyuki Masada
2015	J	`jnl`	Definition and Properties of Direct Sum Decomposition of Groups1. Formaliz. Math. Kazuhisa Nakasho, Hiroshi Yamazaki, Hiroyuki Okazaki, Yasunari Shidama
2015	J	`jnl`	Equivalent Expressions of Direct Sum Decomposition of Groups1. Formaliz. Math. Kazuhisa Nakasho, Hiroyuki Okazaki, Hiroshi Yamazaki, Yasunari Shidama
2015	J	`jnl`	Matrix of ℤ-module1. Formaliz. Math. Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
2015	J	`jnl`	Polynomially Bounded Sequences and Polynomial Sequences. Formaliz. Math. Hiroyuki Okazaki, Yuichi Futa
2015	J	`jnl`	Torsion Part of ℤ-module. Formaliz. Math. Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
2014	J	`jnl`	Difference of Function on Vector Space over F. Formaliz. Math. Kenichi Arai, Ken Wakabayashi, Hiroyuki Okazaki
2014	J	`jnl`	Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module. Formaliz. Math. Kazuhisa Nakasho, Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
2014	J	`jnl`	Torsion Z-module and Torsion-free Z-module. Formaliz. Math. Yuichi Futa, Hiroyuki Okazaki, Kazuhisa Nakasho, Yasunari Shidama
2013	J	`jnl`	Constructing Binary Huffman Tree. Formaliz. Math. Hiroyuki Okazaki, Yuichi Futa, Yasunari Shidama
2013	J	`jnl`	Double Sequences and Limits. Formaliz. Math. Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama
2013	J	`jnl`	Formal definition of probability on finite and discrete sample space for proving security of cryptographic systems using Mizar. Artif. Intell. Res. Hiroyuki Okazaki, Yuichi Futa, Yasunari Shidama
2013	J	`jnl`	Formalization of Definitions and Theorems Related to an Elliptic Curve Over a Finite Prime Field by Using Mizar. J. Autom. Reason. Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
2013	J	`jnl`	Formalization of the Advanced Encryption Standard. Part I. Formaliz. Math. Kenichi Arai, Hiroyuki Okazaki
2013	J	`jnl`	Gaussian Integers. Formaliz. Math. Yuichi Futa, Hiroyuki Okazaki, Daichi Mizushima, Yasunari Shidama
2013	J	`jnl`	Isomorphisms of Direct Products of Cyclic Groups of Prime Power Order. Formaliz. Math. Hiroshi Yamazaki, Hiroyuki Okazaki, Kazuhisa Nakasho, Yasunari Shidama
2013	J	`jnl`	Isomorphisms of Direct Products of Finite Commutative Groups. Formaliz. Math. Hiroyuki Okazaki, Hiroshi Yamazaki, Yasunari Shidama
2013	J	`jnl`	N-Dimensional Binary Vector Spaces. Formaliz. Math. Kenichi Arai, Hiroyuki Okazaki
2013	J	`jnl`	Random Variables and Product of Probability Spaces. Formaliz. Math. Hiroyuki Okazaki, Yasunari Shidama
2013	J	`jnl`	Submodule of free Z-module. Formaliz. Math. Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
2013	J	`jnl`	The Ck Space. Formaliz. Math. Katuhiko Kanazashi, Hiroyuki Okazaki, Yasunari Shidama
2012	J	`jnl`	Banach's Continuous Inverse Theorem and Closed Graph Theorem. Formaliz. Math. Hideki Sakurai, Hiroyuki Okazaki, Yasunari Shidama
2012	J	`jnl`	Extended Euclidean Algorithm and CRT Algorithm. Formaliz. Math. Hiroyuki Okazaki, Yosiki Aoki, Yasunari Shidama
2012	C	`conf`	Formalization of Gaussian integers, Gaussian rational numbers, and their algebraic structures with Mizar. ISITA Yuichi Futa, Daichi Mizushima, Hiroyuki Okazaki
2012	J	`jnl`	Formalization of the Data Encryption Standard. Formaliz. Math. Hiroyuki Okazaki, Yasunari Shidama
2012	J	`jnl`	Free ℤ-module. Formaliz. Math. Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
2012	J	`jnl`	Functional Space Formaliz. Math. Katuhiko Kanazashi, Hiroyuki Okazaki, Yasunari Shidama
2012	J	`jnl`	Higher-Order Partial Differentiation. Formaliz. Math. Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama
2012	J	`jnl`	Isomorphisms of Direct Products of Finite Cyclic Groups. Formaliz. Math. Kenichi Arai, Hiroyuki Okazaki, Yasunari Shidama
2012	J	`jnl`	Operations of Points on Elliptic Curve in Projective Coordinates. Formaliz. Math. Yuichi Futa, Hiroyuki Okazaki, Daichi Mizushima, Yasunari Shidama
2012	J	`jnl`	Posterior Probability on Finite Set. Formaliz. Math. Hiroyuki Okazaki
2012	J	`jnl`	Quotient Module of Z-module. Formaliz. Math. Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
2012	J	`jnl`	Z-modules. Formaliz. Math. Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
2011	J	`jnl`	Banach Algebra of Bounded Complex-Valued Functionals. Formaliz. Math. Katuhiko Kanazashi, Hiroyuki Okazaki, Yasunari Shidama
2011	J	`jnl`	Cartesian Products of Family of Real Linear Spaces. Formaliz. Math. Hiroyuki Okazaki, Noboru Endou, Yasunari Shidama
2011	J	`jnl`	Differentiable Functions into Real Normed Spaces. Formaliz. Math. Hiroyuki Okazaki, Noboru Endou, Keiko Narita, Yasunari Shidama
2011	J	`jnl`	Formalization of Integral Linear Space. Formaliz. Math. Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
2011	J	`jnl`	More on Continuous Functions on Normed Linear Spaces. Formaliz. Math. Hiroyuki Okazaki, Noboru Endou, Yasunari Shidama
2011	J	`jnl`	Normal Subgroup of Product of Groups. Formaliz. Math. Hiroyuki Okazaki, Kenichi Arai, Yasunari Shidama
2011	J	`jnl`	Set of Points on Elliptic Curve in Projective Coordinates. Formaliz. Math. Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
2010	—	`conf`	Formalization of Probability and Random Sampling on a Finite and Discrete Sample Space Using the Mizar Proof Checker. FCS Kenichi Arai, Nobuaki Kondo, Hiroyuki Okazaki
2010	J	`jnl`	Probability Measure on Discrete Spaces and Algebra of Real-Valued Random Variables. Formaliz. Math. Hiroyuki Okazaki, Yasunari Shidama
2009	J	`jnl`	Hopf Extension Theorem of Measure. Formaliz. Math. Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama
2009	J	`jnl`	Probability on Finite Set and Real-Valued Random Variables. Formaliz. Math. Hiroyuki Okazaki, Yasunari Shidama
2009	J	`jnl`	Probability on Finite and Discrete Set and Uniform Distribution. Formaliz. Math. Hiroyuki Okazaki
2009	J	`jnl`	Properties of Primes and Multiplicative Group of a Field. Formaliz. Math. Kenichi Arai, Hiroyuki Okazaki
2008	J	`jnl`	Uniqueness of Factoring an Integer and Multiplicative Group Z/pZ*. Formaliz. Math. Hiroyuki Okazaki, Yasunari Shidama
2007	A	`conf`	An evolutionary multiobjective approach to design highly non-linear Boolean functions. GECCO Hernán E. Aguirre, Hiroyuki Okazaki, Yasushi Fuwa
2005	J	`jnl`	Meta Ring Signature. IACR Cryptol. ePrint Arch. Hiroyuki Okazaki, Ryuichi Sakai, Masao Kasahara
1998	J	`jnl`	Managing the New Telecommunications Paradigms: A Report on APNOMS'98. J. Netw. Syst. Manag. Masayoshi Ejiri, Jong-Tae Park, Hiroyuki Okazaki, James Won-Ki Hong
1996	B	`conf`	On the design and an implementation of broadband access management systems. NOMS T. Kawagoe, H. Kawakami, K. Soga, K. Tanaka, Hiroyuki Okazaki, Satoshi Hasegawa
1993	J	`jnl`	Distributed Self-Healing Control in SONET. J. Netw. Syst. Manag. Hideki Sakauchi, Yasuyo Okanoue, Hiroyuki Okazaki, Satoshi Hasegawa