Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 45

Liczba wyników na stronie
first rewind previous Strona / 3 next fast forward last

Wyniki wyszukiwania

help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 3 next fast forward last
1
Content available remote

Posterior Probability on Finite Set

100%
Okazaki H.
Formalized Mathematics
|
2012
|
tom 20
|
nr 4
257-263
EN
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
Content available remote

Probability on Finite and Discrete Set and Uniform Distribution

100%
Okazaki H.
Formalized Mathematics
|
2009
|
tom 17
|
nr 2
173-178
EN
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
Content available remote

Algebra of Polynomially Bounded Sequences and Negligible Functions

100%
Okazaki H.
Formalized Mathematics
|
2015
|
tom 23
|
nr 4
371-378
EN
In this article we formalize negligible functions that play an essential role in cryptology [10], [2]. Generally, a cryptosystem is secure if the probability of succeeding any attacks against the cryptosystem is negligible. First, we formalize the algebra of polynomially bounded sequences [20]. Next, we formalize negligible functions and prove the set of negligible functions is a subset of the algebra of polynomially bounded sequences. Moreover, we then introduce equivalence relation between polynomially bounded sequences, using negligible functions.
4
Content available remote

Probability Measure on Discrete Spaces and Algebra of Real-Valued Random Variables

64%
Okazaki H., Shidama Y.
Formalized Mathematics
|
2010
|
tom 18
|
nr 4
213-217
EN
In this article we continue formalizing probability and randomness started in [13], where we formalized some theorems concerning the probability and real-valued random variables. In this paper we formalize the variance of a random variable and prove Chebyshev's inequality. Next we formalize the product probability measure on the Cartesian product of discrete spaces. In the final part of this article we define the algebra of real-valued random variables.
5
Content available remote

Properties of Primes and Multiplicative Group of a Field

64%
Arai K., Okazaki H.
Formalized Mathematics
|
2009
|
tom 17
|
nr 2
151-155
EN
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
Content available remote

Formalization of the Data Encryption Standard

64%
Okazaki H., Shidama Y.
Formalized Mathematics
|
2012
|
tom 20
|
nr 2
125-146
EN
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].
7
Content available remote

Probability on Finite Set and Real-Valued Random Variables

64%
Okazaki H., Shidama Y.
Formalized Mathematics
|
2009
|
tom 17
|
nr 2
129-136
EN
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.
8
Content available remote

Uniqueness of Factoring an Integer and Multiplicative GroupZ/pZ*

64%
Okazaki H., Shidama Y.
Formalized Mathematics
|
2008
|
tom 16
|
nr 2
103-107
EN
In the [20], it had been proven that the Integers modulo p, in this article we shall refer as Z/pZ, constitutes a field if and only if Z/pZ is a prime. Then the prime modulo Z/pZ is an additive cyclic group and Z/pZ* = Z/pZ\{0} is a multiplicative cyclic group, too. The former has been proven in the [23]. However, the latter had not been proven yet. In this article, first, we prove a theorem concerning the LCM to prove the existence of primitive elements of Z/pZ*. Moreover we prove the uniqueness of factoring an integer. Next we define the multiplicative group Z/pZ* and prove it is cyclic.MML identifier: INT 7, version: 7.8.10 4.99.1005
9
Content available remote

Formalization of the Advanced Encryption Standard. Part I

64%
Arai K., Okazaki H.
Formalized Mathematics
|
2013
|
tom 21
|
nr 3
171-184
EN
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.
10
Content available remote

N-Dimensional Binary Vector Spaces

64%
Arai K., Okazaki H.
Formalized Mathematics
|
2013
|
tom 21
|
nr 2
75-81
EN
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.
11
Content available remote

Polynomially Bounded Sequences and Polynomial Sequences

64%
Okazaki H., Futa Y.
Formalized Mathematics
|
2015
|
tom 23
|
nr 3
205-213
EN
In this article, we formalize polynomially bounded sequences that plays an important role in computational complexity theory. Class P is a fundamental computational complexity class that contains all polynomial-time decision problems [11], [12]. It takes polynomially bounded amount of computation time to solve polynomial-time decision problems by the deterministic Turing machine. Moreover we formalize polynomial sequences [5].
12
Content available remote

Random Variables and Product of Probability Spaces

64%
Okazaki H., Shidama Y.
Formalized Mathematics
|
2013
|
tom 21
|
nr 1
33-39
EN
We have been working on the formalization of the probability and the randomness. In [15] and [16], we formalized some theorems concerning the real-valued random variables and the product of two probability spaces. In this article, we present the generalized formalization of [15] and [16]. First, we formalize the random variables of arbitrary set and prove the equivalence between random variable on Σ, Borel sets and a real-valued random variable on Σ. Next, we formalize the product of countably infinite probability spaces.
13
Content available remote

Functional SpaceC(ω),C0(ω)

52%
Kanazashi K., Okazaki H., Shidama Y.
Formalized Mathematics
|
2012
|
tom 20
|
nr 1
15-22
EN
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.
14
Content available remote

Z-modules

52%
Futa Y., Okazaki H., Shidama Y.
Formalized Mathematics
|
2012
|
tom 20
|
nr 1
47-59
EN
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].
15
Content available remote

Inferior Limit, Superior Limit and Convergence of Sequences of Extended Real Numbers

52%
Yamazaki H., Endou N., Shidama Y., Okazaki H.
Formalized Mathematics
|
2007
|
tom 15
|
nr 4
231-235
EN
In this article, we extended properties of sequences of real numbers to sequences of extended real numbers. We also introduced basic properties of the inferior limit, superior limit and convergence of sequences of extended real numbers.
16
Content available remote

Hopf Extension Theorem of Measure

52%
Endou N., Okazaki H., Shidama Y.
Formalized Mathematics
|
2009
|
tom 17
|
nr 2
157-162
EN
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].
17
Content available remote

Difference of Function on Vector Space over F

52%
Arai K., Wakabayashi K., Okazaki H.
Formalized Mathematics
|
2014
|
tom 22
|
nr 3
269-275
EN
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.
18
Content available remote

Operations of Points on Elliptic Curve in Projective Coordinates

52%
Futa Y., Okazaki H., Mizushima D., Shidama Y.
Formalized Mathematics
|
2012
|
tom 20
|
nr 1
87-95
EN
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.
19
Content available remote

Conservation Rules of Direct Sum Decomposition of Groups

52%
Nakasho K., Yamazaki H., Okazaki H., Shidama Y.
Formalized Mathematics
|
2016
|
tom 24
|
nr 1
81-94
EN
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.
20
Content available remote

Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module

52%
Nakasho K., Futa Y., Okazaki H., Shidama Y.
Formalized Mathematics
|
2014
|
tom 22
|
nr 3
189-198
EN
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).
first rewind previous Strona / 3 next fast forward last
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ć.