# Search Results

###### Formalization of the Advanced Encryption Standard. Part I

## Summary

In this article, we formalize the Advanced Encryption Standard (AES). AES, which is the most widely used symmetric cryptosystem in the world, is a block cipher that was selected by the National Institute of Standards and Technology (NIST) as an official Federal Information Processing Standard for the United States in 2001 [12]. AES is the successor to DES [13], which was formerly the most widely used symmetric cryptosystem in the world. We formalize the AES algorithm according to [12]. We then verify the correctness of the formalized algorithm that the ciphertext encoded by the AES algorithm can be decoded uniquely by the same key. Please note the following points about this formalization: the AES round process is composed of the SubBytes, ShiftRows, MixColumns, and AddRoundKey transformations (see [12]). In this formalization, the SubBytes and MixColumns transformations are given as permutations, because it is necessary to treat the finite field GF(28) for those transformations. The formalization of AES that considers the finite field GF(28) is formalized by the future article.

###### Properties of Primes and Multiplicative Group of a Field

## Properties of Primes and Multiplicative Group of a Field

In the [16] has been proven that the multiplicative group *Z/pZ*
^{*} is a cyclic group. Likewise, finite subgroup of the multiplicative group of a field is a cyclic group. However, finite subgroup of the multiplicative group of a field being a cyclic group has not yet been proven. Therefore, it is of importance to prove that finite subgroup of the multiplicative group of a field is a cyclic group.

Meanwhile, in cryptographic system like RSA, in which security basis depends upon the difficulty of factorization of given numbers into prime factors, it is important to employ integers that are difficult to be factorized into prime factors. If both *p* and 2*p* + 1 are prime numbers, we call *p* as Sophie Germain prime, and 2*p* + 1 as safe prime. It is known that the product of two safe primes is a composite number that is difficult for some factoring algorithms to factorize into prime factors. In addition, safe primes are also important in cryptography system because of their use in discrete logarithm based techniques like Diffie-Hellman key exchange. If *p* is a safe prime, the multiplicative group of numbers modulo *p* has a subgroup of large prime order. However, no definitions have not been established yet with the safe prime and Sophie Germain prime. So it is important to give definitions of the Sophie Germain prime and safe prime.

In this article, we prove finite subgroup of the multiplicative group of a field is a cyclic group, and, further, define the safe prime and Sophie Germain prime, and prove several facts about them. In addition, we define Mersenne number (*M _{n}*), and some facts about Mersenne numbers and prime numbers are proven.

###### N-Dimensional Binary Vector Spaces

## Summary

The binary set {0, 1} together with modulo-2 addition and multiplication is called a binary field, which is denoted by F2. The binary field F2 is defined in [1]. A vector space over F2 is called a binary vector space. The set of all binary vectors of length n forms an n-dimensional vector space Vn over F2. Binary fields and n-dimensional binary vector spaces play an important role in practical computer science, for example, coding theory [15] and cryptology. In cryptology, binary fields and n-dimensional binary vector spaces are very important in proving the security of cryptographic systems [13]. In this article we define the n-dimensional binary vector space Vn. Moreover, we formalize some facts about the n-dimensional binary vector space Vn.

###### Normal Subgroup of Product of Groups

## Normal Subgroup of Product of Groups

In [6] it was formalized that the direct product of a family of groups gives a new group. In this article, we formalize that for all *j* ∈ *I*, the group *G* = Π_{i∈I}
*G _{i}* has a normal subgroup isomorphic to

*G*. Moreover, we show some relations between a family of groups and its direct product.

_{j}###### Difference of Function on Vector Space over F

## Summary

In [11], the definitions of forward difference, backward difference, and central difference as difference operations for functions on R were formalized. However, the definitions of forward difference, backward difference, and central difference for functions on vector spaces over F have not been formalized. In cryptology, these definitions are very important in evaluating the security of cryptographic systems [3], [10]. Differential cryptanalysis [4] that undertakes a general purpose attack against block ciphers [13] can be formalized using these definitions. In this article, we formalize the definitions of forward difference, backward difference, and central difference for functions on vector spaces over F. Moreover, we formalize some facts about these definitions.

###### Isomorphisms of Direct Products of Finite Cyclic Groups

## Summary

In this article, we formalize that every finite cyclic group is isomorphic to a direct product of finite cyclic groups which orders are relative prime. This theorem is closely related to the Chinese Remainder theorem ([18]) and is a useful lemma to prove the basis theorem for finite abelian groups and the fundamental theorem of finite abelian groups. Moreover, we formalize some facts about the product of a finite sequence of abelian groups.