Composition Security Of Cryptographic Protocols

In recent years, we have witnessed a gradually increasing adoption of crypto-graphic protocols to secure various applications in communications, computer net-works and computer security. However, designing and verifying the security of acomplex cryptographic protocol often proves to be di?cult. Hence, it is alwaysdesirable to be able to use secure and simple protocols as components to composea secure, but larger and more complicated protocol. On the other hand, ubiq-uitous computing environment often results in multiple concurrent executions ofcryptographic protocols. Such condition requires a protocol to be secure and tonot compromise the overall security when it is run concurrently with other proto-cols. Therefore, development of techniques to ensure secure composition of protocolsbecomes inevitable.Among all existing formal methods for cryptographic protocol analysis, theUniversally Composable (UC) framework based on computational complexity andthe DDMP framework based on symbolic analysis (consists of the Protocol Deriva-tion System and the Protocol Composition Logic), are two state-of-the-art proposalsfor security analysis on cryptographic protocols composition. In this dissertation,we select the secure composition of cryptographic protocols as a starting point andcarry out researches on the theories and key technologies in the UC and the DDMPframeworks. The main results are as follows:(1) The provable secure model of identity-based key exchange is proposed in theUC framework. The ideal functionalities of ID-based key exchange are pro-posed with emphasis on ID-based key exchange with Key Generation CenterForward Secrecy (KGC-FS). In addition, the fact that our ID-based KE withKGC-FS functionality can be securely realized by the protocol (with key con-firmation) proposed by Chen and Kudla is proven.(2) The provable security of broadcast authentication using one-time signature isinvestigated in the UC framework. Firstly, a broadcast authentication modelis formulated. Secondly, a UC secure broadcast authentication scheme is pro-posed in the hybrid model. Thirdly, one-time signature protocol HORS+ isproposed. Lastly, protocol OWC is constructed to realize the multi-value regis-tration functionality. Our broadcast authentication scheme constructed by thecombined use of HORS+ and OWC is UC secure and suitable for low-power devices.(3) The Trusted Network Connect (TNC) protocols are analyzed within the UCframework. The TNC model in the UC framework is proposed by first design-ing the TNC ideal functionality, the EAP ideal functionality and the EAP-TNC ideal functionality. Then, a UC secure Trusted Network Connect proto-col named TK-TNC is constructed. Subsequently, a security analysis showsthat D-H PN given in the TCG specification cannot satisfy the UC security andbe resistant to an attack. Using the Twin Di?e-Hellman exchange technique,a UC secure protocol TD-H PN is proposed.(4) The PDS is extended to support the Needham-Schroeder family. Then, thederivation graph of the Needham-Schroeder family is developed by using theextended PDS. In addition, the PCL is applied to prove the correctness ofthe derived protocols. As an example, the detailed derivation and proof ofKerberos Version 5 is shown.