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)

Formalization of Gaussian integers, Gaussian rational numbers, and their algebraic structures with Mizar. - Yuichi Futa; Daichi Mizushima; Hiroyuki Okazaki (ISITA, 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)

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)

Isometric Differentiable Functions on Real Normed Space. - Yuichi Futa; Noboru Endou; 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)

Constructing Binary Huffman Tree. - Hiroyuki Okazaki; Yuichi Futa; 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)

Improving Impossible Differential Cryptanalysis with Concrete Investigation of Key Scheduling Algorithm and Its Application to LBlock. - Jiageng Chen; Yuichi Futa; Atsuko Miyaji; Chunhua Su (NSS, 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)

Topological Properties of Real Normed Space. - Kazuhisa Nakasho; Yuichi Futa; Yasunari Shidama (Formaliz. Math., 2014)

Impossible differential cryptanalysis of LBlock with concrete investigation of key scheduling algorithm. - Jiageng Chen; Yuichi Futa; Atsuko Miyaji; Chunhua Su (IACR Cryptol. ePrint Arch., 2014)

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)

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)

Divisible ℤ-modules. - Yuichi Futa; Yasunari Shidama (Formaliz. Math., 2016)

Lattice of ℤ-module. - Yuichi Futa; Yasunari Shidama (Formaliz. Math., 2016)

Embedded Lattice and Properties of Gram Matrix. - Yuichi Futa; Yasunari Shidama (Formaliz. Math., 2017)

Dual Lattice of ℤ-module Lattice. - Yuichi Futa; Yasunari Shidama (Formaliz. Math., 2017)

Isomorphism Theorem on Vector Spaces over a Ring. - Yuichi Futa; Yasunari Shidama (Formaliz. Math., 2017)

Implicit Function Theorem. Part I. - Kazuhisa Nakasho; Yuichi Futa; Yasunari Shidama (Formaliz. Math., 2017)

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

Continuity of Bounded Linear Operators on Normed Linear Spaces. - Kazuhisa Nakasho; Yuichi Futa; Yasunari Shidama (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)

Inverse Function Theorem. Part I1. - Kazuhisa Nakasho; Yuichi Futa (Formaliz. Math., 2021)

Isomorphism between Spaces of Multilinear Maps and Nested Compositions over Real Normed Vector Spaces. - Kazuhisa Nakasho; Yuichi Futa (Formaliz. Math., 2022)

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)