Composable Analysis And Proof Of Security Protocols

Designing security protocols in the complex Internet environment is a challenging task. Security protocols designed in the stand-alone model may become insecure when running concurrently with other protocols in the Internet. Composable analysis aims at solving such probolems. Composibility is different from other security properties of security protocols. Its emphasis is placed on whether security properties of protocols still remain secure when run concurrently with other protocols. The universally composable security framework is an important tool in the composable analysis of security protocols. This thesis makes deep research into the composable analysis and proof of security protocols in the universally composable security framework. Our research results can be summarized as follows:1 We analyze the design and verification of ideal functionalities in the universally composable security framework. The construction and evolution of the basic password-based key exchange ideal functionality and its'extensions are given using Garay's method. We confirm the validity of Garay's method in the design and verification of the ideal functionality.2 We propose a group key exchange ideal functionality in the universally composable security framework and design a group key exchange protocols securely realizing the ideal functionality based on the tamper-proof hardware token using partially isolated witness indistinguishability. Compared with other protocols under the CRS model, our protocol reduces the risk of putting the whole trust on one point. The group key exchange protocol proposed is proved to be AKE secure against malicious inside attackers. Methods of using tamper-proof hardware in the construction of universally composable security protocols are summarized. Using tamper-proof hardware, protocols can achieve universally composable security and high efficiency at the same time.3 We propose an oblivious pseudorandom permutation evaluation protocol composed of the oblivious polynomial evaluation module and the oblivious pseudorandom function evaluation module. The oblivious pseudorandom permuation evaluation protocol is proved to be secure in the universally composable framework against honest-but-curious attakers. A universally composable password-based key exchange protocol is proposed based on the oblivious pseudorandom permuation evaluation module.4 We substitute one-time signatures with message authentication codes to reduce the bandwidth consumption of Canetti's universally composable key exchange protocol and give a complete proof of the new protocol. Next, we improve the efficiency of oblivious pseudorandom function evaluation module using Applebaum's method based on the assumptions of random distribution of parties'inputs and the difficulty of decoding random linear code. This improvement can finally results in more efficient secure set intersection and pattern matching protocols which use the oblivious pseudorandom function evaluation module.