Formal Model Depiction And Algebraic Property Study For Security Protocol

Formal analyzing is the basic of constructing automated checking tool for security protocol. This thesis studies the problem of model depiction and algebraic property which existents in formal analysis for security protocol mostly, we present the extended type of model and an algorithm of automated realization, analyze related basic theory and application. The main content includes:First, we extend the theory model that based on multiset rewriting. It completes the capacity of examining the type attacking of model by adding new key types and transition rules, extends the capacity of analyzing the non-repudition and fairness of model on the base of adding predication of sending and receiving and function of proof. We choose the Yahalom and Fair-ZG to put up example validation separately.Second, we analysis the intruder deduction problem which follows the algebraic property, bring forward an algorithm of automated realization. Contraposing the presented theories and tools could not deal with the problem of most algebraic equation types now, we study the formal analysis method which based on the theory of term rewriting, and present an algorithm that resolves the intruder deduction problem under equivalent theory. The algorithm is based on the idea of distinguishing equivalent theory and choosing representative elements, it could dispose most intermediator attack which has been discovered that aims at the problem of algebraic property, and progresses an automated checking that takes the BAP.Third, we study the proof of termination of term rewriting theory and application in information security. Compared with the presented polynomial order and lexicographic path order which is difficult to realize automatization or needs much more rules, we give the vector order that based on standardization and vector. The order could not only examine the termination of term rewriting system, but also has the advantage of automated computing and less rules using. Based on the idea of constructing the vector order, we bring forward an algorithm which resolves the problem of XOR equivalent unification, it analyzes all conditions and outputs the unifier when unificated succeed.Finally, we discuss the application of term rewriting theory in security electronic transaction. We give an analysis model based on term rewriting which contraposes the security electronic transaction model that contains many procedures and words. The model has the security of inspecting identity each other between trading men, it meets the totality and consistency, and satisfies the security of authentication and non-repudition.