@phdthesis{oai:sucra.repo.nii.ac.jp:00010406,
 author = {我妻, 和憲},
 month = {},
 note = {vii, 52 p., Many cryptographic protocols have been proposed to securely send and receive information among agents in unsecured networks for various purposes. However, an intruder can eavesdrop secret data and/or impersonate in unsecured cryptographic protocols. Therefore, formal analysis methods of cryptographic protocols such as model checking and theorem proving are used to try to find flaws in the protocols. In formal analysis method such as theorem proving and model checking, analysts firstly enumerate fatal actions of attacks before doing analysis, and then verify whether those attacks succeed or not in communication processes of that target cryptographic protocols. I can say that model checking and theorem proving are formal analysis method with proving because analysts must enumerate target of verification before doing analysis in those methods. In formal analysis method with proving, analysts must enumerate all fatal actions of attacks for target protocol before doing analysis when they verify that target cryptographic protocol is secure. In other words, analysts cannot verify those attacks that are not enumerated before analysis. As an alternative way, a concept of formal analysis with reasoning for cryptographic protocols has been proposed that deduce actions of participants and an intruder from behaviors explicitly and implicitly included in specifications of cryptographic protocols by forward reasoning and detect fatal actions of attacks without enumerated those fatal actions before analysis. Formal analysis method with reasoning is included 3 phases, formalizing specification of a cryptographic protocol, forward reasoning from result of formalization as premises, and analyzing deduced logical formulas by forward reasoning. However, it is difficult for analysts to perform formal analysis with reasoning because its concrete and general steps are not established.
 This paper presents a formal analysis method with reasoning for cryptographic protocols and its supporting tools. At first, I proposed the concrete and general method of formalization, forward reasoning, and analysis in formal analysis method with reasoning. After that, I showed that the proposed method is effective for formal analysis of cryptographic protocols. Finally, I implemented supporting tools in order to perform the proposed method automatically, and evaluated those supporting tools.
 I proposed concrete and general steps of formal analysis method with reasoning for key exchange protocols, and extended the proposed method in order to be applied to various cryptographic protocols. In order to extend the proposed method, at first, I compared 19 kinds of cryptographic protocols based on participants’ behaviors and the number of participants from web site “Cryptographic Protocol Verification Portal,” and a book “Applied Cryptography: Protocols, Algorithms, and Source Code in C” and I found five differences among cryptographic protocols. After that, I extended the proposed method in order to represent those five differences. In order to show effectiveness of the proposed method, at first, I re-detected fatal actions of attacks in target cryptographic protocols that are pointed out by using the proposed method. After that, I chose some cryptographic protocols that include those five differences and performed formal analysis of those cryptographic protocols by the proposed method. As the result, I could perform tasks of the proposed method to the end. Therefore, it can be said that the proposed method can apply to detect fatal actions of attacks that represent success of attack in 19 cryptographic protocols. In order to support tasks of the proposed method, I implemented supporting tools that are inputted specification of target cryptographic protocol, and perform tasks of the proposed method automatically, and output the result whether attacks succeed or not. Finally, I evaluated whether duration in the tasks can be reduced by using those supporting tools, compared to a case that analysts perform the proposed method manually.
 As the result of showing effectiveness of the proposed method, at first, I could redetect fatal actions of attacks that represent success of attack that is pointed out. Therefore, I showed that the proposed method can detect fatal actions of attacks that represent success of attack. After that, in formal analysis of some cryptographic protocols that include five differences among cryptographic protocols, I could perform tasks of the proposed method to the end. Therefore, I showed that the proposed method can be applied to those 19 cryptographic protocols. As the result of evaluation of implemented supporting tools, I showed that analysts can reduce duration of the proposed method by using those supporting tools.
 Structure of this thesis is as follows. Chapter 1 presents background, motivation, and purpose of this research. Chapter 2 explains formal analysis of cryptographic protocols. Chapter 3 proposes formal analysis method with reasoning for key exchange protocols. Chapter 4 presents extending the proposed formal analysis method with reasoning for key exchange protocols. Chapter 5 shows effectiveness of the proposed method. Chapter 6 presents supporting tools for the proposed method and evaluation of those supporting tools. Chapter 7 presents discussion of the proposed method and implemented supporting tools. Finally, concluding remarks are given in Chapter 8., Abstract i
Acknowledgments iii
List of figures vi
List of tables vii
1 Introduction 1
1.1 Background and Motivation . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Purposes and Objectives . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.3 Structure of This Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . 2
2 Formal Analysis of Cryptographic Protocols 3
2.1 Cryptographic Protocols . . . . . . . . . . . . . . . . . . . . . . . . . 3
2.2 Formal Analysis Method with Proving . . . . . . . . . . . . . . . . . . 4
2.3 Formal Analysis Method with Reasoning . . . . . . . . . . . . . . . . 5
3 Formal Analysis Method with Reasoning for Key Exchange Protocols 7
3.1 Key Exchange Protocols . . . . . . . . . . . . . . . . . . . . . . . . . 7
3.2 Tasks of Formalization . . . . . . . . . . . . . . . . . . . . . . . . . . 8
3.2.1 Overview of Formalization . . . . . . . . . . . . . . . . . . . . 8
3.2.2 Behavior of Participants . . . . . . . . . . . . . . . . . . . . . 12
3.2.3 Behavior of an Intruder . . . . . . . . . . . . . . . . . . . . . . 14
3.2.4 Common Behavior among Participants and an Intruder . . . . . 15
3.2.5 Irregular Case . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
3.3 Forward Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.4 Tasks of Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
3.5 Applying the Proposed Method to Otway-Rees Protocol . . . . . . . . . 19
4 Extending Proposed Formal Analysis Method with Reasoning for Key Exchange
Protocols 22
4.1 Comparison of Cryptographic Protocols . . . . . . . . . . . . . . . . . 22
4.2 Formalization of Cryptographic Protocols . . . . . . . . . . . . . . . . 24
4.2.1 Overview of Formalization . . . . . . . . . . . . . . . . . . . . 24
4.2.2 Behavior of Participants . . . . . . . . . . . . . . . . . . . . . 24
4.2.3 Behavior of an Intruder . . . . . . . . . . . . . . . . . . . . . . 26
4.2.4 Common Behavior among Participants and an Intruder . . . . . 27
4.2.5 Irregular Case . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
4.3 Forward Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
4.4 Tasks of Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
5 Demonstration of Effectiveness 32
5.1 Method of Demonstration . . . . . . . . . . . . . . . . . . . . . . . . . 32
5.2 Case in Secret Splitting Protocols . . . . . . . . . . . . . . . . . . . . . 32
5.3 Case in Coin Flips Protocols . . . . . . . . . . . . . . . . . . . . . . . 35
6 Supporting Tools for Proposed Method 37
6.1 Requirement Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
6.2 Overview of Supporting Tools . . . . . . . . . . . . . . . . . . . . . . 39
6.3 Implementation of Supporting Tools . . . . . . . . . . . . . . . . . . . 40
6.4 Evaluation of Supporting Tools . . . . . . . . . . . . . . . . . . . . . . 42
7 Discussion 44
8 Conclusions 46
8.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
8.2 Future Works . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
Publications 48
References 50, 指導教員 : 程京徳, text, application/pdf},
 school = {埼玉大学},
 title = {A Formal Analysis Method with Reasoning for Cryptographic Protocols and Its Supporting Tools},
 year = {2016},
 yomi = {ワガツマ, カズノリ}
}