Formal Analysis Of Security Protocols Based On Universally Composable Framework

The analysis and verification of security protocols are important techniques to guarantee the security properties and the application requirements. Formal methods and automated tools are both necessary and effective for those purpose. Nevertheless, most of the existing formal methods abstract away symbolic operations from concrete cryptographic primitives, yet without justifying the correctness of the abstractions. Thus, they cannot be used to prove that the protocols preserve security properties when symbolic operations were substituted by corresponding concrete cryptographic primitives.Recently, many different approaches have been proposed for cryptographically sound symbolic analysis. Among others, the universally composable symbolic analysis (UCSA) framework layers Dolev-Yao style symbolic analysis on top of the universally composable (UC) security framework to construct general computationally sound proofs of security protocols. UCSA maps each symbolic cryptographic operation in Dolev-Yao model to an ideal functionality in the UC framework, resulting in simpler proofs for cryptographically soundness at the same time. However, only a restricted class of sequentially which employ standard public-key encryption and digital signature, such as mutual authentication and key exchange protocols ,can be analyzed in the original UCSA. This thesis intends to extend the framework, the main results are listed as follows:1. We define an framework for formal analysis of security protocols based on the probabilistic applied pi-calculus (PAPi). On the one hand, the process calculus, as a descriptive language, captures precisely the interactive characteristic of the protocols. On the other hand, the probabilistic choice operator in the PAPi enables protocols in the formal model to make probabilistic selection in behavioral level, thus enlarged the class of protocols which can be modeled and analyzed.2. We add new assumptions on network communication to the framework, such as adversary-controlled communication (bare model communication), authenticated communication, anonymous communication. Each assumption is characterized by a number of auxiliary processes. Therefore, we could choose for different protocols different communication models.3. We extend the supported cryptographic primitives. In particular, two-party primitive protocol, such as blind signature protocol and commitment protocol, are embedded into the framework. Each primitive is modeled by auxiliary processes which corresponds to some ideal functionality.4. We reformulate the definition of simple protocol in the UC framework in accordance with the extension of the formal analysis framework.5. As a case study, we give the traditional criterion both in the formal analysis framework and the UC functionality of the UC framework for coin-tossing protocol, and describe the relationship between the criterion and the ideal functionality.