Research On Methods Of Security Assurance Based On Computer-Assisted Proof

Along with the comprehensive application of computers and network, many protocols and software which seem to be safe and correct show serious security problems. These problems are brought during their process of design and implement. So some proper and systematic methods are needed urgently to strengthen such security. This thesis gives a deep investigation on the methods of security assurance, proposes a resolution plan based on computer-assisted proof. Then we evaluate its feasibility and validity in both theoretical and practical ways.Firstly, this thesis makes an analysis and comparison of the current formal methods and computer-assisted proof tools, points out the advantages and disadvantages separately. Then wechoose the inductive proof assistant——Coq which is based on higher order logic as theplatform of our study. We analyse the powerful function of Coq based on the in-depthinvestigation of Coq's meta language——Calculus of Inductive Constructions. It provides thetheoretical foundation and technical support for Coq based security assurance. After that, we establish different formal models for stop-wait protocol and Otway-Rees authentication protocol, formalize the relative concepts and properties, and make a strict computer-assisted proof for both of them. The result shows that the stop-wait protocol is faultless in design and there is type flaw in Otway-Rees protocol. At last, the thesis gives a study on Hoare logic and technologies such as program extraction for verification of the correctness of programs. We explore a systematic way to offer security assurance for programs after verifying many functional and imperative programs by Coq.The formalizations and proofs are verified strictly by computer-assisted prover. The processes and results of these verifications show that method based on computer-assisted proof can provide security assurance for protocols and software systematically and effectively.