Algorithms for cryptographic protocol verification in presence of algebraic properties.

摘要

The design of cryptographic protocols is error-prone, people have found flaws in seemingly secure protocols years after they were proposed. Therefore formal methods are needed to give a more formal guarantee that protocols are secure. In general, there are two approaches: the formal-model approach and the computational-model approach. This dissertation follows the line of the formal-model approach. Traditionally, the formal-model approach assumes the perfect encryption assumption, which means no information can possibly be released out of any encrypted message without knowing the key. But this is not true in general, there are protocols where cryptographic primitives have certain algebraic properties. This dissertation aims to relax the perfect encryption assumption.In Chapter 2, we propose a framework of rigid theorem proving modulo a flexible theory. Using this framework, we give a decision procedure for solving the prefix theory and the blind signature theory. In Chapter 3, we formulate the insecurity problem of protocols as a Cap Unification problem. We give a decision procedure for Cap Unification when the convergent system defining the intruder abilities is dwindling, with some additional assumptions satisfied by usual protocols. In Chapter 4, we extend our work in Chapter 3, we give a decision procedure for Cap Unification when the intruder capacities are modeled as homomorphic encryption theories. This is done by adding two things to the decision procedure in Chapter 3: a unification procedure modulo the homomorphic encryption theory, and some inference rules designed to deal with the homomorphic encryption theory.