Distributed Self-Healing Control in SONET. - Hideki Sakauchi; Yasuyo Okanoue; Hiroyuki Okazaki; Satoshi Hasegawa (J. Netw. Syst. Manag., 1993)

On the design and an implementation of broadband access management systems. - T. Kawagoe; H. Kawakami; K. Soga; K. Tanaka; Hiroyuki Okazaki; Satoshi Hasegawa (NOMS, 1996)

Managing the New Telecommunications Paradigms: A Report on APNOMS'98. - Masayoshi Ejiri; Jong-Tae Park 001; Hiroyuki Okazaki; James Won-Ki Hong (J. Netw. Syst. Manag., 1998)

Meta Ring Signature. - Hiroyuki Okazaki; Ryuichi Sakai; Masao Kasahara (IACR Cryptol. ePrint Arch., 2005)

An evolutionary multiobjective approach to design highly non-linear Boolean functions. - Hernán E. Aguirre; Hiroyuki Okazaki; Yasushi Fuwa (GECCO, 2007)

Uniqueness of Factoring an Integer and Multiplicative Group Z/pZ*. - Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2008)

Properties of Primes and Multiplicative Group of a Field. - Kenichi Arai; Hiroyuki Okazaki (Formaliz. Math., 2009)

Hopf Extension Theorem of Measure. - Noboru Endou; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2009)

Probability on Finite and Discrete Set and Uniform Distribution. - Hiroyuki Okazaki (Formaliz. Math., 2009)

Probability on Finite Set and Real-Valued Random Variables. - Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2009)

Formalization of Probability and Random Sampling on a Finite and Discrete Sample Space Using the Mizar Proof Checker. - Kenichi Arai; Nobuaki Kondo; Hiroyuki Okazaki (FCS, 2010)

Probability Measure on Discrete Spaces and Algebra of Real-Valued Random Variables. - Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2010)

Formalization of Integral Linear Space. - Yuichi Futa; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2011)

Set of Points on Elliptic Curve in Projective Coordinates. - Yuichi Futa; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2011)

Banach Algebra of Bounded Complex-Valued Functionals. - Katuhiko Kanazashi; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2011)

Normal Subgroup of Product of Groups. - Hiroyuki Okazaki; Kenichi Arai; Yasunari Shidama (Formaliz. Math., 2011)

Differentiable Functions into Real Normed Spaces. - Hiroyuki Okazaki; Noboru Endou; Keiko Narita; Yasunari Shidama (Formaliz. Math., 2011)

More on Continuous Functions on Normed Linear Spaces. - Hiroyuki Okazaki; Noboru Endou; Yasunari Shidama (Formaliz. Math., 2011)

Cartesian Products of Family of Real Linear Spaces. - Hiroyuki Okazaki; Noboru Endou; Yasunari Shidama (Formaliz. Math., 2011)

Formalization of Gaussian integers, Gaussian rational numbers, and their algebraic structures with Mizar. - Yuichi Futa; Daichi Mizushima; Hiroyuki Okazaki (ISITA, 2012)

Isomorphisms of Direct Products of Finite Cyclic Groups. - Kenichi Arai; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2012)

Higher-Order Partial Differentiation. - Noboru Endou; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2012)

Operations of Points on Elliptic Curve in Projective Coordinates. - Yuichi Futa; Hiroyuki Okazaki; Daichi Mizushima; Yasunari Shidama (Formaliz. Math., 2012)

Z-modules. - Yuichi Futa; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2012)

Quotient Module of Z-module. - Yuichi Futa; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2012)

Free ℤ-module. - Yuichi Futa; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2012)

Functional Space C(ω), C0(ω). - Katuhiko Kanazashi; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2012)

Posterior Probability on Finite Set. - Hiroyuki Okazaki (Formaliz. Math., 2012)

Extended Euclidean Algorithm and CRT Algorithm. - Hiroyuki Okazaki; Yosiki Aoki; Yasunari Shidama (Formaliz. Math., 2012)

Formalization of the Data Encryption Standard. - Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2012)

Banach's Continuous Inverse Theorem and Closed Graph Theorem. - Hideki Sakurai; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2012)

Formal definition of probability on finite and discrete sample space for proving security of cryptographic systems using Mizar. - Hiroyuki Okazaki; Yuichi Futa; Yasunari Shidama (Artif. Intell. Res., 2013)

N-Dimensional Binary Vector Spaces. - Kenichi Arai; Hiroyuki Okazaki (Formaliz. Math., 2013)

Formalization of the Advanced Encryption Standard. Part I. - Kenichi Arai; Hiroyuki Okazaki (Formaliz. Math., 2013)

Double Sequences and Limits. - Noboru Endou; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2013)

Gaussian Integers. - Yuichi Futa; Hiroyuki Okazaki; Daichi Mizushima; Yasunari Shidama (Formaliz. Math., 2013)

Submodule of free Z-module. - Yuichi Futa; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2013)

The Ck Space. - Katuhiko Kanazashi; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2013)

Constructing Binary Huffman Tree. - Hiroyuki Okazaki; Yuichi Futa; Yasunari Shidama (Formaliz. Math., 2013)

Random Variables and Product of Probability Spaces. - Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2013)

Isomorphisms of Direct Products of Finite Commutative Groups. - Hiroyuki Okazaki; Hiroshi Yamazaki; Yasunari Shidama (Formaliz. Math., 2013)

Isomorphisms of Direct Products of Cyclic Groups of Prime Power Order. - Hiroshi Yamazaki; Hiroyuki Okazaki; Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2013)

Formalization of Definitions and Theorems Related to an Elliptic Curve Over a Finite Prime Field by Using Mizar. - Yuichi Futa; Hiroyuki Okazaki; Yasunari Shidama (J. Autom. Reason., 2013)

Difference of Function on Vector Space over F. - Kenichi Arai; Ken Wakabayashi; Hiroyuki Okazaki (Formaliz. Math., 2014)

Torsion Z-module and Torsion-free Z-module. - Yuichi Futa; Hiroyuki Okazaki; Kazuhisa Nakasho; Yasunari Shidama (Formaliz. Math., 2014)

Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module. - Kazuhisa Nakasho; Yuichi Futa; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2014)

Application to Women's Healthcare of Health Management System Using a Tablet Phone. - Hiroyuki Okazaki; Hiroki Matsumoto; Yoshiki Shibata; Shinichi Motomura; Naoyuki Masada (BIH, 2015)

Matrix of ℤ-module1. - Yuichi Futa; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2015)

Torsion Part of ℤ-module. - Yuichi Futa; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2015)

Equivalent Expressions of Direct Sum Decomposition of Groups1. - Kazuhisa Nakasho; Hiroyuki Okazaki; Hiroshi Yamazaki; Yasunari Shidama (Formaliz. Math., 2015)

Definition and Properties of Direct Sum Decomposition of Groups1. - Kazuhisa Nakasho; Hiroshi Yamazaki; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2015)

Algebra of Polynomially Bounded Sequences and Negligible Functions. - Hiroyuki Okazaki (Formaliz. Math., 2015)

Polynomially Bounded Sequences and Polynomial Sequences. - Hiroyuki Okazaki; Yuichi Futa (Formaliz. Math., 2015)

Formalization of Polynomially Bounded and Negligible Functions Using the Computer-Aided Proof-Checking System Mizar. - Hiroyuki Okazaki; Yuichi Futa (FM4M/MathUI/ThEdu/DP/WIP@CIKM, 2016)

Formalization of statistical indistinguishability of probability distribution ensembles in Mizar. - Hiroyuki Okazaki (ISITA, 2016)

Privacy Preserving Logic Formula Calculation in Cloud. - Hiroshi Yamaguchi; Shigeo Tsujii; Hiroyuki Okazaki; Yasunari Shidama (ICSC, 2016)

Conservation Rules of Direct Sum Decomposition of Groups. - Kazuhisa Nakasho; Hiroshi Yamazaki; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2016)

Suitable Symbolic Models for Cryptographic Verification of Secure Protocols in ProVerif. - Hiroyuki Okazaki; Yuichi Futa; Kenichi Arai (ISITA, 2018)

Binary Representation of Natural Numbers. - Hiroyuki Okazaki (Formaliz. Math., 2018)

Operations of Points on Elliptic Curve in Affine Coordinates. - Yuichi Futa; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2019)

Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm. - Hiroyuki Okazaki; Koh-ichi Nagao; Yuichi Futa (Formaliz. Math., 2019)

Formal Verification of Merkle-Damgård Construction in ProVerif. - Takehiko Mieno; Togo Yoshimura; Hiroyuki Okazaki; Yuichi Futa; Kenichi Arai (ISITA, 2020)

Virtual Environment for Analysis and Evaluation of DDoS Attacks. - Ryo Tokuyama; Yuichi Futa; Hikofumi Suzuki; Hiroyuki Okazaki (AINA (3), 2021)

Real Vector Space and Related NotionsThis study was supported in part by JSPS KAKENHI Grant Numbers 17K00182 and 20K19863. - Kazuhisa Nakasho; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2021)

Finite Dimensional Real Normed Spaces are Proper Metric Spaces. - Kazuhisa Nakasho; Hiroyuki Okazaki; Yasunari Shidama (Formaliz. Math., 2021)

The 3-Fold Product Space of Real Normed Spaces and its Properties. - Hiroyuki Okazaki; Kazuhisa Nakasho (Formaliz. Math., 2021)

Formalization of Orthogonal Decomposition for Hilbert Spaces. - Hiroyuki Okazaki (Formaliz. Math., 2022)

On the Formalization of Gram-Schmidt Process for Orthonormalizing a Set of Vectors. - Hiroyuki Okazaki (Formaliz. Math., 2023)

Formal Security Verification for Searchable Symmetric Encryption Using ProVerif. - Takehiko Mieno; Hiroyuki Okazaki; Kenichi Arai; Yuichi Futa; Hiroaki Yamamoto (ISITA, 2024)

How to Formalize Loop Iterations in Cryptographic Protocols Using ProVerif. - Takehiko Mieno; Hiroyuki Okazaki; Kenichi Arai; Yuichi Futa (IEEE Access, 2024)

Formalization of Orthogonal Complements of Normed Spaces. - Hiroyuki Okazaki (Formaliz. Math., 2024)