In recent years, formal veri cation applications have attracted signi cant attention. In particular, veri cation of the security of cryptosystems has been investigated extensively. In this study, we attempt to develop various mathematical libraries for cryptology using the Mizar proof checking system. Polynomially bounded and negligible functions play very important roles in cryptology. Therefore, we introduce formalized de nitions of polynomially bounded and negligible functions for formalizing cryptology in Mizar.
In recent years, formal veri cation applications have attracted signi cant
attention. Veri cation of the security of cryptosystems is has been investigated
extensively. The objective of this study is to develop mathematical libraries to verify
the security of cryptographic systems using the Mizar proof checking system [
are difficult to solve if the input size is sufficiently large. It is well known that
polynomial-time problems can be solved with a relatively low computational
cost. We consider a problem Pa to be as hard to solve as another problem Pb
if we can solve Pb by calling the algorithm that can solve Pa a polynomially
bounded number of times. We are interested in the formalization of
computational complexities. Polynomially bounded functions play an important role in
practical computational complexity theory. The class P is a fundamental
computational complexity class that contains all polynomial-time decision problems
[
To analyze the security of cryptographic primitives such as symmetric
encryption or hash functions as well as that of cryptographic protocols, we evaluate
the success probability of any attack against them. In general, a cryptosystem
is secure if the probability of any attack succeeding against the cryptosystem is
negligible. Therefore, we formalize a rigorous de nition of the negligible
functions [
In this paper, we rst introduce our formalized de nition of polynomially
bounded functions. Next, we formalize the de nition of negligible functions and
prove that the set of negligible functions is a subset of the set of polynomially
bounded functions. Moreover, we introduce an equivalence relationship between
polynomially bounded functions using negligible functions. All formalized de
nitions and theorems in this paper are described in the Mizar language, and their
proofs are veri ed by the Mizar proof checker. Our formal descriptions have been
stored in the current version of the Mizar Mathematical Library (MML)⋆ and
are available online on the Mizar Project official website [
Asymptotic notations allow us to describe the behavior of given real-valued
functions. In particular, O notation is often used to analyze the increase in
realvalued functions and to classify the computational complexity of solving the
given problems. Fortunately, there are formal de nitions and theorems
regarding asymptotic notation in the MML. Therefore, we can use these de nitions
to offer a formalized de nition of polynomially bounded functions that do not
increase faster than polynomials. We then formalize some theorems regarding
polynomially bounded functions. Next, we formalize the de nition of negligible
functions that do not decrease slower than the multiplicative inverses of
polynomials and formalize some theorems about them. It is well known that linear
combinations of polynomially bounded functions are also polynomially bounded
and that those of negligible functions are also negligible. These facts are very
useful for evaluating computational complexity and for proving the security of
cryptosystems. Thus, we formalize proofs for these theorems. Speci cally, we
⋆ Indexed by the MML identi ers ASYMPT 2[
Mizar [
In this section, we brie y review the asymptotic O notation and introduce related formal de nitions available in the MML. For our purposes (i.e., computer science and cryptology) it is sufficient to analyze the behavior of discrete functions. In fact, asymptotic notation in the MML is formalized on sequences, which are synonymous with functions whose domains comprise natural numbers. De nition: 1 Let f ( ) and g( ) be functions from N to R. g( ) 2 O (f ( )) iff 9N is a natural number and c is a real number s.t. 8n s.t. N n holds 0 g(n) c f (n).
The O notation is de ned in Mizar as follows: De nition: 2 (ASYMPT_0:def 9) definition let f be
eventually-nonnegative Real_Sequence; func Big_Oh(f) -> FUNCTION_DOMAIN of NAT,REAL
equals { t where t is Element of Funcs(NAT, REAL) : ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0}; end; In Mizar, Real Sequence is an alias for a function from N to R and \eventuallynonnegative" is an attribute for Real Sequence and is de ned as follows: De nition: 3 (ASYMPT_0:def 2) definition let f be Real_Sequence; attr f is eventually-nonnegative means ex N being Nat st for n being Nat st n >= N holds f.n >= 0; end; De nition: 4 (ASYMPT_1:def 3) definition let a be Real; func seq_n^(a) -> Real_Sequence means it.0 = 0 & for n st n > 0 holds
it.n = n to_power a;
The sequence of the monomial f (n) = na is de ned in Mizar as follows: The sequence of the exponential ab n+c, where a; b; and c are given constant real numbers, is de ned in Mizar as follows: De nition: 5 (ASYMPT_1:def 1) definition let a,b,c be Real; func seq_a^(a,b,c) -> Real_Sequence means it.n = a to_power (b*n+c); end; Note that for a given real number x, f (n) = xn is represented as \seq a^(x,1,0)" in Mizar. 3.2
De nition: 6 A real valued function, f ( ), is polynomially bounded if there exists a natural number, k, such that f (x) 2 O (xk) (n) < De nition: 7 Let ( ) be a function from N to R. ( ) is a (negligible function) iff for all polynomial p( ) holds 9N be a natural number s.t. 8n be a natural number s.t. N n holds
In this section, we introduce our formal de nitions of polynomially bounded functions and polynomial functions. 4.1
De nition: 8 (ASYMPT_2:def 1) definition let p be Real_Sequence; attr p is polynomially-bounded means ex k be Nat st
p in Big_Oh(seq_n^(k)); This de nition may appear very similar to Def. 6 but is only a formalization of an attribute for real sequences. In the Mizar language, attributes are constructors of adjectives. We can de ne an attribute followed by the keyword \attr". Def. 6 gives only a de nition of an attribute for real-valued functions. However, formal methods never accept the declaration of new objects without an evidence of their existence in order to eliminate any errors in proofs. In the Mizar system, there are several ways to treat polynomially bounded functions. One is to prove that declared real sequences satisfy the de nition of being polynomially bounded. Another way is to prove the existence of polynomially bonded functions and to de ne a new mode for polynomially bounded sequences as a sub mode of a \Real Sequence". It should be noted that in the Mizar language, \mode" is similar to \type" used in other languages. Furthermore, all modes are derived from the mode \set" because the Mizar system is based on the set theory. The third option is to de ne a set of speci c functions and their algebraic structure as new terms. We will show an example of the third case in Sec. 6.
Theorem: 1 (ASYMPT_2:25) theorem for a be Nat st 1 < a holds seq_a^(a,1,0) is non polynomially-bounded; This theorem shows that the exponential f (x) = ax is not polynomially bounded if 1 < a. We rst prove Theorem 2 as a lemma for proving Theorem 1. The following theorem holds that 2x is nonpolynomially bounded: Theorem: 2 (ASYMPT_2:16) theorem
for x be Nat st 1 < x holds not ex N,c be Nat st for n be Nat st N <= n holds 2 to_power n <= c * (n to_power x); To prove Theorem 2, we assume that the proposition of Theorem 1 is not true and derive a contradiction against Theorem 2. The actual formal proof of Theorem
4.2
Although polynomials have been formalized in the MML [
De nition: 9 (ASYMPT_2:def 2) definition let c be XFinSequence of REAL; func seq_p(c) -> Real_Sequence means for x be Nat holds it.x = Sum(c (#) seq_a^(x,1,0)); end; \XFinSequence" is a nite sequence whose indices start from 0. In this de nition, XFinSequence c is the given coefficient for the representation of a polynomial. For example, (seq p(<*a,b,c*>)).x = a + bx + cx2. Note that this de nition formalizes \func seq p(c) ", where \func" is a keyword that shows that the term is de ned as a FUNCTOR. In the Mizar language, FUNCTOR plays the role of a constructor of new terms. To de ne a FUNCTOR, the proof checker requires proofs of at least the existence and uniqueness of the new term. In this case, once we call \seq p(c)", the checker automatically recognizes this term as a Real Sequence. We can then refer to the de ning theorem, \for x be Nat holds it.x = Sum(c (#) seq a^(x,1,0))" to prove another theorem. We will discuss the usage of FUNCTOR in Sec. 6.
Theorem: 3 (ASYMPT_2:45) theorem for k be Nat, c be XFinSequence of REAL st len c = k+1 & 0 < c.k holds seq_p(c) in Big_Oh( seq_n^(k) ); This theorem holds that any kth-degree polynomial function whose most significant coefficient is positive is of O(nk). Theorem 4 follows Theorem 3: Theorem: 4 (ASYMPT_2:46) theorem for k be Nat, c be XFinSequence of REAL st len c = k+1 & 0 < c.k holds
seq_p(c) is polynomially-bounded;
theorem holds that 2 x is a negligible function: De nition: 10 (ASYMPT_3:def 4) definition let f be Function of NAT,REAL; attr f is negligible means for c be non empty positive-yielding
XFinSequence of REAL holds ex N be Nat st for x be Nat st N <=x holds |. f.x .| < 1/((seq_p(c)).x); end; Theorem: 5 (ASYMPT_3:25) theorem for f be Function of NAT,REAL st for x be Nat holds
f.x = 1/ (2 to_power x) f is negligible; holds Theorem: 6 (ASYMPT_3:24) theorem for f be Function of NAT,REAL st f is negligible holds f is convergent & lim f = 0;
By providing a formal proof of correctness, we can automate inference rules ( i.e., namely clusters) in the MML as follows: registration let f be negligible Function of NAT,REAL, a be Real; cluster a(#)f -> negligible
for Function of NAT,REAL; end; registration let f,g be negligible Function of NAT,REAL; cluster f+g -> negligible
for Function of NAT,REAL; end; registration let f,g be negligible Function of NAT,REAL; cluster f(#)g -> negligible
for Function of NAT,REAL; end; registration let f be negligible Function of NAT,REAL, g be polynomially-abs-bounded
Function of NAT,REAL; cluster g(#)f -> negligible
for Function of NAT,REAL; end Once these clusters are registered, the checker automatically infers that addition and scalar multiplication between negligible functions yield negligible results. For example, the Mizar proof checker inferences the following theorem automatically:
for a be Real, e,f be negligible Real_Sequence, g be polynomially-abs-bounded
Real_Sequence holds (a (#) f)(#) g + e is negligible;
In general, a cryptosystem is secure if the probability of a successful attack against the cryptosystem is negligible. To prove this, we evaluate the total sum of the probability of success of any possible attack. Adversaries are allowed to attack in parallel or iteratively. In most cases, it is sufficient to evaluate the linear combination of probabilities of successful attacks if the probability of all attacks is negligible. We have formalized de nitions and theorems concerning probability and probability distributions that can treat concrete probabilistic events for describing attacks against cryptosystems [2{7]. In combination with these formal descriptions, the above-mentioned clusters would be useful for formal veri cation of the security of cryptosystems.
In Secs. 4 and 5, we introduced our formalizations of polynomially bounded functions and negligible functions. In this section, we propose a formal de nition of the algebra of polynomially bounded functions and present some theorems about negligible functions and this algebra. 6.1
Set of polynomially bounded functions First, we de ne a relaxed attribute of polynomially bounded functions namely \polynomially-abs-bounded", as follows: De nition: 11 (ASYMPT_3:def 1) definition
let p be Real_Sequence; attr p is polynomially-abs-bounded means ex k be Nat st |. p .| in Big_Oh(seq_n^(k)); end; Here, j. p .jis the absolute value of the given function p. Although we de ne the attribute polynomially-bounded in Sec. 8, we formalize this de nition for technical reasons, i.e., in order to introduce the multiplicative inverse of addition between polynomially bounded functions. Naturally, polynomially bounded functions are polynomially-abs-bounded. We then register the following clusters: registration cluster polynomially-bounded -> polynomially-abs-bounded for Real_Sequence; end; Next, we de ne the set of polynomially-abs-bounded functions as a new term, namely, \Big Oh poly", as follows: De nition: 12 (ASYMPT_3:def 2) definition func Big_Oh_poly -> Subset of RAlgebra (NAT) means for x being object holds x in it iff x is polynomially-abs-bounded
Function of NAT,REAL;
registration
cluster Big_Oh_poly -> non empty; end; In other words, we made the proof-checker recognize the existence of polynomiallyabs-bounded functions. Algebraic structure of polynomially bounded functions In this section, we de ne the algebraic structure of polynomially bounded functions as follows: De nition: 13 (ASYMPT_3:def 3) definition func R_Algebra_of_Big_Oh_poly
-> strict AlgebraStr means the carrier of it = Big_Oh_poly & the multF of it
= (RealFuncMult(NAT)) || Big_Oh_poly & the addF of it
= (RealFuncAdd(NAT)) || Big_Oh_poly & the Mult of it = (RealFuncExtMult(NAT))
| [:REAL,Big_Oh_poly:] & the OneF of it
= RealFuncUnit(NAT) & the ZeroF of it
= RealFuncZero(NAT); In this formalization, we de ne the carrier, multiplication, addition, scalar multiplication, multiplicative unit, and additive unit. The carrier of R Algebra of Big Oh poly (i.e., Big Oh poly) is included in the set of all real-valued functions. Instead of de ning a new operation, we use prede ned operations on real-valued functions by restricting their domain according to the carrier of this structure. We de ne the additive and multiplicative units of this structure as being the same as those of the algebra of real-valued functions.
We then prove the attributes that are held by the algebraic structure R Algebra of Big Oh poly, and register them as the following cluster: registration cluster R_Algebra_of_Big_Oh_poly -> strict Abelian add-associative right_zeroed right_complementable commutative associative right_unital right-distributive vector-associative scalar-associative vector-distributive scalar-distributive; end;
Theorem: 8 (ASYMPT_3:18) theorem
R_Algebra_of_Big_Oh_poly is Algebra;
In this section, we de ne the set of negligible functions as a new term, namely, \negligibleFuncs", as follows: De nition: 14 (ASYMPT_3:def 5) definition func negligibleFuncs ->
Subset of Big_Oh_poly means for x being object holds x in it iff x is negligible Function of NAT,REAL; end;
registration
cluster negligibleFuncs -> non empty; end; Note that we de ne \negligibleFuncs" as a nonempty subset of R Algebra of Big Oh poly.
Equivalence between polynomially bounded functions We de ne the following predicate: De nition: 15 (ASYMPT_3:def 6) definition let f,g be Function of NAT,REAL; pred f negligibleEQ g means ex h be Function of NAT,REAL st
h is negligible & for x be Nat holds
|. f.x - g.x .| <= |.h.x.|; reflexivity; symmetry; end; Here \f negligibleEQ g" means that there exists a negligible function, h, which is the upper bound of the difference between two functions, f and g. In other words, we introduce an equivalence relationship between polynomially bounded functions. This equivalence would be useful not only for cryptography and computer science but also for approximating and analyzing functions.
Theorem: 9 (ASYMPT_3:39) theorem for v,w be
VECTOR of R_Algebra_of_Big_Oh_poly st w in negligibleFuncs holds v * w in negligibleFuncs; where VECTOR is a synonym for an element of the structure, and \v * w" is the product of two VECTORs v and w: (v w):x = (v:x) (w:x). This theorem shows that the product \v * w" of two functions is negligible if v is a polynomially bounded function and w is a negligible function. Recall the above mentioned theorems and clusters concerning negligible functions. The set of negligible functions is a nonempty subset of the set of polynomially bounded functions. Addition and scalar multiplication between negligible functions also yield negligible functions. These theorems mean that the set of negligible functions is an ideal of the set of polynomially bounded functions. 7
In this section, we show an example of evaluating the computational cost of
algorithms. In [
theorem for a,b be Element of INT st |.a.| > |.b.| & b > 1 holds ex A,B be sequence of NAT,
C be Real_Sequence,
n be Element of NAT st A.0 = |.a.| & B.0 = |.b.| & (for i be Nat holds A.(i+1) = B.i & B.(i+1) = A.i mod B.i) & n = (min*{i where i is Nat: B.i = 0} ) & a gcd b = A.n & Fib(n+1) <= |. b .| & n <= 5*[/ log(10,|. b .|) \] &
n <= C.(|. b .|) & C is polynomially-bounded; In future works, we will formalize complex algorithms that include iterations or subroutine calls even though we were able to formalize the Euclidean algorithm using simple sequences. 8
In this section, we brie y describe our future plans for formalizing the security of cryptologic systems. It is well known that the security of cryptosystems is dependent on the complexity of computational problems. Polynomially bounded functions play an essential role in evaluating and classifying the complexity of computational problems. We are attempting to formalize computational complexity using our libraries mentioned in Sec. 4.
ne other cryptologic topics using our formalization of probability distribution.
Currently, we are attempting to formalize the indistinguishability of probability
distributions. In modern cryptology, the security of cryptologic systems is
essentially de ned by indistinguishability. For example, various cryptologic topics,
such as pseudo-random number generators and hash functions, are described
using the concept of indistinguishability. We often design a cryptographic scheme
by employing ideal functions. However, we must replace such ideal functions
with feasible functions when we implement the schemes. Thus, an implemented
scheme is not always secure even if its ideal functionality has been proven to be
secure in design. Indistinguishability of functions means the indistinguishability
of the distributions of the outputs of the functions between an ideal function
(e.g., an ideal random function) and a feasible function (e.g., a hash function)
to prove the security of a cryptographic scheme. Two probability distributions
are statistically indistinguishable if the distance between them is negligible. We
intend to de ne a formalization of indistinguishability using our formalization
of negligible functions mentioned in Sec. 5 and probability distributions[
In this paper, we introduced a formalized de nition of polynomially bounded and negligible functions in the Mizar language. We then showed formalized theorems related to these de nitions. All formalized de nitions and theorems in this paper are described in the Mizar language, and the proofs of these theorems have been veri ed using the Mizar proof checker. Our formal descriptions have been stored in the current version of the MML and are available online on the Mizar Project official website. We prepared these formalized articles in order to achieve our aim of constructing an automated formal veri cation tool for cryptology. We will now attempt to formalize one of the most important concepts of cryptology indistinguishability using the formalization of negligible functions introduced in this paper.
This study is partly supported by JSPS KAKENHI 15K00183. The authors would like to express their gratitude to Prof. Yasunari Shidama for his support and encouragement.