Kazuhisa Nakasho, Yuichi Futa and Yasunari Shidama

Formalized Mathematics 25(4) 269-282 Jan 2018 [Refereed]

An analysis attack with distributions is one of attacks against cipher schemes.
The attack need mathematical tools such as implicit functions and their properties. On the other hand, formalization has become important for security evaluation agai...

Isomorphism Theorem on Vector Spaces over a Ring

Yuichi Futa and Yasunari Shidama

Formalized Mathematics 25(3) 171-178 Dec 2017 [Refereed]

In development of cryptosystems, security proof for their security evaluation is necessary. Formal verification with computers is important to avoid error in the proof. However, the formalization of mathematical definitions and theorems for secur...

In development of cryptosystems, security proof for their security evaluation is necessary. Formal verification with computers is important to avoid error in the proof. However, the formalization of mathematical definitions and theorems for secur...

Embedded Lattice and Properties of Gram Matrix

Yuichi Futa and Yasunari Shidama

Formalized Mathematics 25(1) 73-86 May 2017 [Refereed]

In development of cryptosystems, security proof for their security evaluation is necessary. Formal verification with computers is important to avoid error in the proof. However, the formalization of mathematical definitions and theorems for secu...

Lattice of Z-modules

Yuichi Futa and Yasunari Shidama

Formalized Mathematics 24(1) 37-47 Aug 2016 [Refereed]

In development of cryptosystems, security proof for their security evaluation is necessary. Formal verification with computers is important to avoid error in the proof. However, the formalization of mathematical definitions and theorems for secur...