| ABSTRACT | 第1-9页 |
| 摘要 | 第9-10页 |
| Chapter 1 INTRODUCTION | 第10-16页 |
| ·Background | 第10-12页 |
| ·Related Work | 第12-14页 |
| ·Our Contribution | 第14页 |
| ·Structure of the Thesis | 第14-16页 |
| Chapter 2 PRELIMINARIES OF MPCS | 第16-22页 |
| ·Description of MPCS | 第16-17页 |
| ·Desirable Properties | 第17-18页 |
| ·Cryptographic Primitives | 第18-22页 |
| ·Theory of Private Contract Signatures | 第18-20页 |
| ·Private Contract Signatures in MPCS | 第20-22页 |
| Chapter 3 FORMAL MODEL FOR MPCS | 第22-28页 |
| ·Concurrent Game Structures and ATL | 第22-23页 |
| ·Model-Checker Mocha | 第23-25页 |
| ·Modelling MPCS Protocols in Mocha | 第25-26页 |
| ·Expressing Properties of MPCS Protocols in ATL | 第26-27页 |
| ·Summary | 第27-28页 |
| Chapter 4 MODEL CHECKING MR PROTOCOLS | 第28-42页 |
| ·Description of MR Protocols | 第28-32页 |
| ·Main Protocol | 第28-29页 |
| ·Sub-Protocols | 第29-32页 |
| ·Automatic Analysis of MR Protocols | 第32-41页 |
| ·MR Models | 第32-37页 |
| ·Analysis Results | 第37-38页 |
| ·Comparison With the Verification in NuSMV | 第38-41页 |
| ·Summary | 第41-42页 |
| Chapter 5 MODEL CHECKING MRT PROTOCOLS | 第42-63页 |
| ·Design Methodology of MRT Protocols | 第42-44页 |
| ·Design MRT Protocols with 3 and 4 Signers | 第44-49页 |
| ·Description of MRT Protocols | 第49-51页 |
| ·Main Protocol | 第49-50页 |
| ·Resolve Sub-Protocol | 第50-51页 |
| ·Automatic Analysis of MRT Protocols | 第51-62页 |
| ·MRT Models | 第52-55页 |
| ·A Fairness Attack on The Instance Protocol | 第55-57页 |
| ·An Abuse-Freeness Flaw | 第57-62页 |
| ·Summary | 第62-63页 |
| Chapter 6 CONCLUSION | 第63-65页 |
| ·Main Work | 第63-64页 |
| ·Future Research | 第64-65页 |
| BIBLIOGRAPHY | 第65-70页 |
| 致谢 | 第70-71页 |
| PUBLICATIONS | 第71-72页 |
| 学位论文评阅及答辩情况表 | 第72页 |
