In [14] we formalized probability and probability distribution on a finite sample space. In this article first we propose a formalization of the class of finite sample spaces whose element’s probability distributions are equivalent with each other. Next, we formalize the probability measure of the class of sample spaces we have formalized above. Finally, we formalize the sampling and posterior probability.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
A pseudorandom number generator plays an important role in practice in computer science. For example: computer simulations, cryptology, and so on. A pseudorandom number generator is an algorithm to generate a sequence of numbers that is indistinguishable from the true random number sequence. In this article, we shall formalize the "Uniform Distribution" that is the idealized set of true random number sequences. The basic idea of our formalization is due to [15].
3
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In the various branches of science, probability and randomness provide us with useful theoretical frameworks. The Formalized Mathematics has already published some articles concerning the probability: [23], [24], [25], and [30]. In order to apply those articles, we shall give some theorems concerning the probability and the real-valued random variables to prepare for further studies.
4
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article we formalize DES (the Data Encryption Standard), that was the most widely used symmetric cryptosystem in the world. DES is a block cipher which was selected by the National Bureau of Standards as an official Federal Information Processing Standard for the United States in 1976 [15].
5
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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 2p + 1 are prime numbers, we call p as Sophie Germain prime, and 2p + 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 (Mn), and some facts about Mersenne numbers and prime numbers are proven.
6
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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.
7
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article, we formalize some basic facts of Z-module. In the first section, we discuss the rank of submodule of Z-module and its properties. Especially, we formally prove that the rank of any Z-module is equal to or more than that of its submodules, and vice versa, and that there exists a submodule with any given rank that satisfies the above condition. In the next section, we mention basic facts of linear transformations between two Z-modules. In this section, we define homomorphism between two Z-modules and deal with kernel and image of homomorphism. In the last section, we formally prove some basic facts about linearly independent subsets and linear combinations. These formalizations are based on [9](p.191-242), [23](p.117-172) and [2](p.17-35).
8
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article, we formalize a torsion Z-module and a torsionfree Z-module. Especially, we prove formally that finitely generated torsion-free Z-modules are finite rank free. We also formalize properties related to rank of finite rank free Z-modules. The notion of Z-module is necessary for solving lattice problems, LLL (Lenstra, Lenstra, and Lov´asz) base reduction algorithm [20], cryptographic systems with lattice [21], and coding theory [11].
9
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
The authors have presented some articles about Lebesgue type integration theory. In our previous articles [12, 13, 26], we assumed that some σ-additive measure existed and that a function was measurable on that measure. However the existence of such a measure is not trivial. In general, because the construction of a finite additive measure is comparatively easy, to induce a σ-additive measure a finite additive measure is used. This is known as an E. Hopf's extension theorem of measure [15].
10
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article, first we give a definition of a functional space which is constructed from all complex-valued continuous functions defined on a compact topological space. We prove that this functional space is a Banach algebra. Next, we give a definition of a function space which is constructed from all complex-valued continuous functions with bounded support. We also prove that this function space is a complex normed space.
11
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article, we formalize Z-module, that is a module over integer ring. Z-module is necassary for lattice problems, LLL (Lenstra-Lenstra-Lovász) base reduction algorithm and cryptographic systems with lattices [11].
12
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
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.
13
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article we formalize one of the most important theorems of linear operator theory - the Closed Graph Theorem commonly used in a standard text book such as [10] in Chapter 24.3. It states that a surjective closed linear operator between Banach spaces is bounded.
14
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article we formalize a free ℤ-module and its rank. We formally prove that for a free finite rank ℤ-module V , the number of elements in its basis, that is a rank of the ℤ-module, is constant regardless of the selection of its basis. ℤ-module is necessary for lattice problems, LLL(Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic systems with lattice [15]. Some theorems in this article are described by translating theorems in [21] and [8] into theorems of Z-module.
15
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article, conservation rules of the direct sum decomposition of groups are mainly discussed. In the first section, we prepare miscellaneous definitions and theorems for further formalization in Mizar [5]. In the next three sections, we formalized the fact that the property of direct sum decomposition is preserved against the substitutions of the subscript set, flattening of direct sum, and layering of direct sum, respectively. We referred to [14], [13] [6] and [11] in the formalization.
16
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article we formalize a quotient module of Z-module and a vector space constructed by the quotient module. We formally prove that for a Z-module V and a prime number p, a quotient module V/pV has the structure of a vector space over Fp. Z-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lov´asz) base reduction algorithm and cryptographic systems with lattices [14]. Some theorems in this article are described by translating theorems in [20] and [19] into theorems of Z-module.
17
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article, we formalize operations of points on an elliptic curve over GF(p). Elliptic curve cryptography [7], whose security is based on a difficulty of discrete logarithm problem of elliptic curves, is important for information security. We prove that the two operations of points: compellProjCo and addellProjCo are unary and binary operations of a point over the elliptic curve.
18
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article, we shall extend the formalization of [10] to discuss higher-order partial differentiation of real valued functions. The linearity of this operator is also proved (refer to [10], [12] and [13] for partial differentiation).
19
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
In this article we formalize some number theoretical algorithms, Euclidean Algorithm and Extended Euclidean Algorithm [9]. Besides the a gcd b, Extended Euclidean Algorithm can calculate a pair of two integers (x, y) that holds ax + by = a gcd b. In addition, we formalize an algorithm that can compute a solution of the Chinese remainder theorem by using Extended Euclidean Algorithm. Our aim is to support the implementation of number theoretic tools. Our formalization of those algorithms is based on the source code of the NZMATH, a number theory oriented calculation system developed by Tokyo Metropolitan University [8].
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.