| With the rapid development of computer network and the information security technology, the transaction process of an electronic commerce activity appeared more complex, which a transaction possibly involves many buyers or sellers. In order to realize multi-party security exchange, various multi-party security protocols is proposed, such as multi-party non-repudiation protocol, multi-party fair exchange protocol, multi-party authentication mail protocols, multi-party contract signing protocols. Compared with the general security protocol, the complexity of multi-party security protocols increased greatly. Its requests of efficiency characteristic such as bandwidth are become more and more high, and more complex cryptology foundation is need.Therefore, the process of design and the formalized analysis of multi-party security protocol is more complex, and it has become an important research direction of the information security.The multi-party security protocol is constructed by the basic safety methods. The choice of different technology will be able to affect finally multi-party security protocol efficiency, security and so on. Except using traditional safety technology of data encryption and digital signature, the group encryption scheme, verifiable secret sharing scheme (VSS), signcryption and threshold signcryption technology is more often used in multi-party security protocol. The group encryption is a technology based on CRT and public key cryptography, it produces a group key which can only be used by members. Secret sharing is an important method of information security and data security, and VSS is a basic tool of the multi-party security protocol design. Signcryption can realizes signs and encryption simultaneously in a step, and can eliminate the communication bottleneck which produced by using the trusted third party(TTP), and in this way it can enhances the security protocol (including two-party and multi-party protocols, especially multi-party security protocol) operating efficiency greatly.The dissertation has studied these related technologies of multi-party security protocols firstly, and then some typical multi-party security protocols are introduced.Multi-party security protocol is related to many kind of technologies of cryptology and information security, there are some flaws inevitably in the design of multi-party security protocol. There are a lot of theory and methods to study security protocol at present, and formalized method is the main way to analysis multi-party security protocol. The formalized method is mainly divided into three kinds: formal logic method based on knowledge and belief, model checking method and theorem proof method. The dissertation mainly studies the logical formalized method and its applications in formal analysis of multi-party security protocols, especially study the SVO logic improvement and its application in multi-party security protocol analysis. We also have made some research of game-based ATL logic method and its applications in multi-party security protocols analysis. In general, we have studies the related formal analysis technologies of multi-party security protocols from two aspects, theory and applications. The main works and results are as follows: 1.We have studied technologies of group encryption, verifiable secret sharing scheme (VSS) and signcryption, which is related to multi-party security protocols and play a very important role in the multi-party security protocol design and improvement. The threshold-based signs technology is also studied, and a (t,n) threshold unsigncryption scheme based on the ECC is proposed. The scheme not only provides lower computation and communication, but also have message confidentiality, authentication, unforgeability, non-repudiation, resistance of malicious verifiers cheating others and etc., so it satisfies the request of group communication.2. The logical formalization methods of security protocol analysis are studied. The SVO logic's basic symbol, inference rule, inference process, semantics and characteristics is mainly studied, and pointed out that SVO logic urgently needs to improve when it is used to analysis security protocols(include two-party and multi-party security protocols).3. In order to enable the SVO logic be used in analyzing non-repudiation, timeless, fairness and Hash function's description of two-party or multi-party security protocols, several formalization extended methods of the SVO logic have been studied systematically. The new ZG non-repudiation protocol is formal analyzed by using the inference rule of extended SVO logic.4. A new formalized analysis method based on the SVO logic is studied. The inference rule of the new method is rewrite with the standard SVO logic basic symbols and few mistakes of the new method is corrected, so that it can be easily used in formal analysis of two-party or multi-party security protocols. In addition, we have proposed a new SVO logic extended method and used it to formal analysis of a new electronic payment protocol.5. The SVO logic and its expansion is not only used to analysis safety of simple security protocols, but also used to analysis the non-repudiation, fairness, timeless, authentication based on Hash function of the complex multi-party security protocols. We have done some research for this, the non-repudiation of a multi-party non-repudiation protocol without TTP and the fairness of a double group encrypted key multi-party non-repudiation protocol is separately formal analyzed by using axiom and inference rules of SVO logic.6. We have made some research of game-based ATL logic method and its applications in formalized analysis of multi-party security protocols. The famous Markowitch-Kremer multi-party non-repudiation protocol is modeled and analyzed by using ATL logic and model-checking tool MOCHA, and a fairness flaw is found.We have improved this multi-party non-repudiation protocol by add time limit to each participant, and enable it to have fairness and timeless simultaneously.
|
PDF Full Text Request