Formalization Of Finite Field GF(2^n) Based On Coq And It's Application

The finite field GF(2~n) is the basis of many security-critical algorithms.It plays an important role in AES encryption algorithms,elliptic curve encryption,infection function masks,and so on.Operations on finite fields are prone to errors due to their complexity,and these problems can make a system fail.Verification methods,which are based on testing and model checking,can only be performed on algorithms of finite fields with a bounded n.When n is large,it is difficult to obtain effective and comprehensive verification.The formal verification based on interactive theorem provers provides a possibility of making a generic verification of operations of finite fields,but it is very difficult to work in this area.The working process of the verification method based on theorem proof is similar to that of mathematical theorem.First,the researchers need to establish a set of definitions and prove a batch of lemmas,and then prove the final goal on the basis of these prerequisite work,so the researchers first need to complete the corresponding mathematical theory formalize in the theorem prover to build a formal library of mathematical theories.The main goal of this paper is to build a formal mathematical library of finite fieldGF(2~n),including constructive definition of related concepts of finite field,and formal verification of some properties of the field based on the constructive definition.In response to these problems,this paper uses the theorem prover Coq to formally defines the elements on the finite fieldsGF(2~n)and basic operations on them,then formalizes a set of basic properties related to finite fieldsGF(2~n),including the verification of basic properties of finite field addition,and partial properties of finite field multiplication,etc.This work laid a foundation for the complete formalization of finite fields and the formal verification of algorithms based on finite fields.This paper considers several methods to achieve formal verification of finite fields.The main research results are as follows:First of all,this paper formally defines a special finite fieldGF(2~8).On this basis,the paper finishes formal verification.This finite field is mainly used in the AES algorithm,which is a difficult point in the formal verification of the AES algorithm.After that,the paper extends the properties that formal verified,and used them to finish the formal verification of the difficult Mix Columns in the AES algorithm.Then,in view of the limitations of the previous work,this paper uses an inductive structure as the carrier of the elements on the finite fieldGF(2~n),and uses recursion as the main means to finish the formal definition of operations on the finite fieldGF(2~n).The definition finished in this way is applicable to finite fieldsGF(2~n)of arbitrary size and arbitrary structure.After that,this paper formally verifications the relevant properties of finite fieldsGF(2~n).In addition,the formal verification of the basic properties of addition exchange law,combination law,unit element,and inverse element has been finished.In terms of multiplication,because direct verification is difficult,this article is divided into several parts.At present,the formal verification of the related properties of the polynomial multiplication and the properties of modulo operation constituting the finite fieldGF(2~n)multiplication has been finished.On this basis,the formal verification of some properties of finite field multiplication is finished.This paper mainly verifies by introduction,and the properties obtained are applicable to finite fieldsGF(2~n)of arbitrary size and arbitrary structure.The formal mathematical library formed in this study can also help other research.Finally,this article gives three examples of practical applications of the above work.First,the properties of the finite fieldGF(2~8)are extended,and the extended properties are used to finish the formal verification of the difficult Mix Columns in the AES algorithm.The specific application of the formal definition of the finite field is finished.Then,using the results obtained in this paper to formal define a special formalization of the finite fieldGF(2~n),and formalize the program using this part of the calculation.Finally,an example of applying the properties of formal verification in this paper to actual operation is shown,and a complex finite field operation problem is formalized verification using the properties verified in this paper.These three examples show the specific use of the work in this paper and the practicality of this work.