Formal Theories And Methods For Security Protocol Analysis

A safe cryptographic protocol is one of absolutely necessary components of the communication of networks and its applications, and it is the basis of composing information security systems. The main tasks of Protocol Engineering (PE) include designing safe and efficient cryptographic protocols. In the procedures of PE, which include design, description (modeling), verification, performance analysis, implement, test and maintenance, protocol verification is one of the key procedures. The analysis and synthesis of protocols are two efficient approaches to verify protocols;the former is more efficient than the latter.Since the 1970's, some formal theories of cryptographic protocol analysis have been proposed, which cover Dolev-Yao model, modal logic, Paulson's induction, strand space model, spi-calculus theory and so on. On the basis of these theories, formal methods of cryptographic protocol analysis, such as logic proving, model checking, theorem proving and type checking, have been introduced. By the former two methods, the insecurity of cryptographic protocols can be only got, but the safety of security objectives cannot be got. The last method has a defect for security objectives to be verified incompletely. By theorem proving, security objectives of cryptographic protocols may be proved.In this paper, we studied formal theories and methods based on theorem proving for cryptographic protocol analysis. They include characters of the term and event space, the denotation of the principal process, the classification and formal description of security objectives and the security problem of cryptographic protocols. Our main contributions are as follows.1. Characters of the term space are investigated, and theories and methods for qualitative and quantitative analysis of the architecture of terms are proposed. Encryption and concatenation of terms, inverse keys operator and f-operator on the set of terms are defined, by which all kinds of terms of principals including attackers are produced. Sets of terms and their operators are written as term algebra, whose operation laws and sub-term relations are tools of qualitative and quantitative analysis of the architecture of terms respectively.2. Characters of the event space are investigated, and the theory for dynamic analysis of exchanged messages is proposed. Sequences of events can be the semanticmodel of prefixing operator of processes, which arc equal to indexed principal events of the set of events by causal predecessor. Its corresponding reachable path marks the course of the typed unit of transferred terms. The decidable theorem of the primary protocol independent to its corresponding secondary protocols in the combination of protocols that run in a concurrent way is proposed.3. On the basis of the theory of process algebra such as spi-calculus, the denotation of principal processes of cryptographic protocols that run in a concurrent way is investigated, and a process description language is proposed, in a which, the semantic model of prefixing, parallel composition and choice operator of principal processes can be the composition of sequences of principal events, the communication of sequences of principal events, and M-division of event sets with paths among principal events respectively. Moreover, the algorithm of principal process calculus and its bi-simulation relation are proposed.4. The event graph model for formal cryptographic protocols that run in a concurrent way is proposed. In this model, there are three restrictions that include the communication and causal predecessor between events and freshness of terms. A sub-graph that meets all three restrictions is written as a metal-graph, which is a component of composing event graphs. The algorithm of composing event graphs introduced via the definition of operators between events and metal-graphs respectively. The bi-simulation equivalent relation of event graphs is maintained as a measure of bi-simulation of metal-graphs. On the basis of the bi-simulation equivalent relation of event graphs, rules for eliminating redundancy of event graphs are developed. The event graph model can be a combination of spi-calculus and strand space theory and its extension.5. A novel method of proving security objectives is proposed according to the theory of decidable honesty of global smallest X-ideals. On the basis of encryption and concatenation of terms, inverse keys operator and ^operator on the set of terms, a invariant set i.e. smallest .K-ideal is defined, and the theorem of decidable honesty of invariants and its demonstration are proposed. Moreover, the theorem of satisfiability for decidable conditions of honest ideals and the algorithm for composing smallest /C-ideals are introduced. Our work is contributed to extend the strand space theory.Moreover, the classification principle of security objectives based on their architectures, dependent relations of security objectives and their independent proposition are proposed.