Universally Composable Symbolic Analysis Of Non-repudiation Protocols

Formal methods become tremendously important in the analysis of security protocols in order to meet nowadays'increasing demand of internet security requirement. However, most existing formal methods abstract away symbolic operations from concrete cryptographic primitives. Thus, it cannot guarantee that the protocol which has been proved to be secure in a formal method remains its security in the real world. The framework UCSA (Universally Composable Symbolic Analysis), proposed by Canetti, constructing general computationally sound proofs of security protocols. After that, Luo extended UCSA into a framework based on PAPi calculus which can handle new communication channel assumptions and new cryptographic primitives. This thesis extends Luo's framework to deal with new security requirements– non-repudiation. The main contributions are threefold:Firstly, we add resilient authentication communication channel assumption to the UCSA framework so that it can handle the non-repudiation requirement. In order to achieve this, we define a respective assistant process and the ideal functionality for the resilient communication channels and prove the soundness and completeness between them. We extend the simple protocol, adversary strategy and protocol event defined in UCSA to model the new assumption.Secondly, we use the framework to analyze Zhou-Gollmann protocol to check whether it satisfies the non-repudiation requirement with and without resilient communication assumption. It applies UCSA to analyze a concrete protocol ever since it was devised. This thesis models every participant in the ZG protocol and translates the simple protocol into respective symbolic protocol.Finally, we prove that ZG protocol without resilient communication assumption does not meet the security requirement of non-repudiation protocols while ZG protocol with resilient communication assumption does.