Computer Science

Computer Science ›› 2020, Vol. 47 ›› Issue (12): 311-318.doi: 10.11896/jsjkx.190900197

Previous Articles     Next Articles

Formalization of Finite Field GF(2n) Based on COQ

FAN Yong-qian, CHEN Gang, CUI Min   

  1. College of Computer Science and Technology Nanjing University of Aeronautics and Astronauitcs Nanjing 211000,China
    Key Laboratory of Safety-critical Software Ministry of Industry and Information Technology Nanjing 211106,China
  • Received:2019-09-29 Revised:2020-03-09 Published:2020-12-17
  • About author:FAN Yong-qian,born in 1993postgraduateis a student member of China Computer Federation.His main research interests include formal methods and so on.
    CHEN Gang,born in 1958Ph.Dprofessoris a senior member of China Computer Federation.His main research interests include formal methods and so on.

PDF (PC)

738

Abstract: The finite field GF(2n) is the basis of many security-critical algorithmsincluding AES encryption algorithmselliptic curve cryptographyinfection function masksand so on.There is data that the operations on the finite field are prone to errors due to their complexitywhich causes problems in the system.Verification methods based on testing and model checking can only be applied on specific finite field with fixed by nand the computation time for the verification often exceeds the capability of the computer.Formal verification using interactive theorem provers provides the possibility for generic verification of finite field pro-pertiesbut working in this direction fairly challenging.The existing researches mainly focused on the formal verification of abstract properties of finite fieldshoweversolving practical problems require the use of constructive definitions of finite fields and the verification of its properties.In response to this requirementthis paper uses the theorem prover COQ to develop a constructive and generic definition of finite field GF(2n)and formally verified a large amount basic properties of finite fieldsincluding verification of the basic properties of finite field additionverification of the basic properties of polynomial multiplication which is the buliding block of finite field multiplicationas well as verification of other related properties.This work lays a foundation for the complete formalization of finite fieldswhich will support formal verfications of various algorithms using finite field.

Key words: COQ, Finite field, Formal verification, Polynomial operation, Theorem proving

CLC Number: 

  • TP311
[1] MCELIECE R J.Finite fields for computer scientists and engineers[M].Springer Science &Business Media,2012.
[2] DAEMEN J,RIJMEN V.The design of Rijndael:AES-the advanced encryption standard[M].Springer Science &Business Media,2013.
[3] HANKERSON D,MENEZES A J,VANSTONE S.Guide to elliptic curve cryptography[M].Springer Science &Business Media,2006.
[4] OSHIDA H,UENO R,HOMMA N,et al.On Masked Galois-Field Multiplication for Authenticated Encryption Resistant to Side Channel Analysis[C]//International Workshop on Constructive Side-Channel Analysis and Secure Design.Cham:Springer,2018:44-57.
[5] PHILIPOOM J.Correct-by-construction finite field arithmetic in Coq[D].Cambridge:Massachusetts Institute of Technology ,2018.
[6] INRIA.Coq Ring Theory[DB/OL].[2019-09-02].https://coq.inria.fr/distrib/current/stdlib/Coq.setoid_ring.Ring_theory.html.
[7] INRIA.Coq Field Theory[DB/OL].[2019-09-02].https://coq.inria.fr/distrib/current/stdlib/Coq.setoid_ring.Field_theory.html.
[8] GONTHIER G,MAHBOUBI A,RIDEAU L,et al.A modular formalisation of finite group theory[C]//International Confe-rence on Theorem Proving in Higher Order Logics.Berlin:Springer,2007:86-101.
[9] YU C,CIESIELSKI M.Formal Analysis of Galois Field Arithmetic Circuits-Parallel Verification and Reverse Engineering[J].IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,2018,38(2):354-365.
[10] YU C,CIESIELSKI M.Efficient parallel verification of galois field multipliers[C]//2017 22nd Asia and South Pacific Design Automation Conference (ASP-DAC).IEEE,2017:238-243.
[11] PAAR C,FLEISCHMANN P,ROELSE P.Efficient multiplier architectures for Galois fields GF (2/sup 4n/)[J].IEEE Transactions on Computers,1998,47(2):162-170.
[12] LV J,KALLA P,ENESCU F.Verification of composite Galois field multipliers over GF ((2m)n) using computer algebra techniques[C]//2011 IEEE International High Level Design Validation and Test Workshop.IEEE,2011:136-143.
[13] TEAM T C D.The Coq Proof Assistant Reference Manual-Version V8.7.1[C]//INRIA.2016.
[14] BERTOT Y,CASTÉRAN P.Interactive theorem proving and program development:Coq'Art:the calculus of inductive constructions[M].Springer Science &Business Media,2013.
[15] ANDRONICK J,CHETALI B,LY O.Using coq to verify java
card tm applet isolation properties[C]//International Conference on Theorem Proving in Higher Order Logics.Berlin:Springer,2003:335-351.
[16] GONTHIER G.Formal proof-the four-color theorem[J].Notices of the AMS,2008,55(11):1382-1393.
[17] BLANQUI F,COUPET-GRIMAL S,DELOBEL W,et al.CoLoR:a Coq Library on Rewriting and termination[C]//Eighth International Workshop on Termination (WST2006).Seattle,United States,2006.
[18] OKAZAKI H,ARAI K,SHIDAMA Y.Formal Verification of AES Using the Mizar Proof Checker[C]//Proceedings of the 2012 International Conference on Foundations of Computer Science (FCS'12).2012:78-84.
[19] ARAI K,OKAZAKI H.Formalization of the Advanced Encryption Standard.Part I[J].Formalized Mathematics,2013,21(3):171-184.
[20] LIDL R,NIEDERREITER H.Finite fields[M].Cambridge:Cambridge University Press,1997.
[21] COLLINS G E.Computing multiplicative inverses in GF(p)[J].Mathematics of Computation,1969,23(105):197-200.
[22] ILIEV A,KYURKCHIEV N,RAHNEV A.A Note on Adaptation of the Knuth's Extended Euclidean Algorithm for Computing Multiplicative Inverse[J].International Journal of Pure and Applied Mathematics,2018,118(2):281-290.
[23] WIKIPEDIA.Rijndael MixColumns[DB/OL].[2019-04-17].https://en.wikipedia.org/wiki/Rijndael_MixColumns.
[1] JIAN Qi-rui, CHEN Ze-mao, WU Xiao-kang. Authentication and Key Agreement Protocol for UAV Communication [J]. Computer Science, 2022, 49(8): 306-313.
[2] WANG Ran-ran, WANG Yong, CAI Yu-tong, JIANG Zheng-tao, DAI Gui-ping. Formal Verification of Yahalom Protocol Based on Process Algebra [J]. Computer Science, 2021, 48(6A): 481-484.
[3] SUN Xiao-xiang, CHEN Zhe. Study on Correctness of Memory Security Dynamic Detection Algorithm Based on Theorem Proving [J]. Computer Science, 2021, 48(1): 268-272.
[4] LI Ling, LI Huang-hua, WANG Sheng-yuan. Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design [J]. Computer Science, 2020, 47(6): 8-15.
[5] MA Zhen-wei,CHEN Gang. Matrix Formalization Based on Coq Record [J]. Computer Science, 2019, 46(7): 139-145.
[6] CHEN Hao, LUO Lei, LI Yun, CHEN Li-rong. Study on Formal Verification of Secure Virtual Machine Monitor [J]. Computer Science, 2019, 46(3): 170-179.
[7] WEI Wan-yin, DU Xiao-ni, LI Zhi-xia and WAN Yun-qi. Linear Complexity of Quaternary Generalized Cyclotomic Sequences with Period pq [J]. Computer Science, 2017, 44(6): 174-176.
[8] WEI Qing and SUN Guang-hong. Class of Permutation Polynomials over Finite Fields [J]. Computer Science, 2017, 44(5): 170-171.
[9] ZHU Xian-wei, ZHU Zhi-qiang and SUN Lei. Design and Formal Verification of Xen Hybrid Multi-police Model [J]. Computer Science, 2017, 44(10): 134-141.
[10] LI Shan-shan, ZHAO Chun-na, GUAN Yong, SHI Zhi-ping, WANG Rui, LI Xiao-juan and YE Shi-wei. Formalization of Consistency of Fractional Calculus in HOL4 [J]. Computer Science, 2016, 43(3): 23-26.
[11] LI Yan-chun, LI Xiao-juan, GUAN Yong, WANG Rui, ZHANG Jie and WEI Hong-xing. xMAS-based Formal Verification of SpaceWire Credit Logic [J]. Computer Science, 2016, 43(2): 113-117.
[12] YANG Xiu-mei, GUAN Yong, SHI Zhi-ping, WU Ai-xuan, ZHANG Qian-ying and ZHANG Jie. Higher-order Logic Formalization of Function Matrix and its Calculus [J]. Computer Science, 2016, 43(11): 24-29.
[13] CHEN Li-rong, LI Yun and LUO Lei. Research on Formal Verification of Embedded Operating System [J]. Computer Science, 2015, 42(8): 203-214.
[14] LV Xing-li, SHI Zhi-ping, LI Xiao-juan, GUAN Yong, YE Shi-wei and ZHANG Jie. Higher-order Logic Formalization of Basic Theory of Continuous Fourier Transform [J]. Computer Science, 2015, 42(4): 31-36.
[15] WU Gui-ming, ZHENG Fang, XIE Xiang-hui, WU Dong and YAN Xin-kai. Hardware Implementation of Scalar Multiplication on Elliptic Curves over GF(2m) [J]. Computer Science, 2015, 42(1): 79-81.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.