What does it mean for a cryptographic protocol to be “secure”? Capturing security properties of cryptographic protocols in a meaningful way is a slippery business: On the one hand, we want to guarantee that a security property holds in face of “all feasible attacks” against a protocol. On the other hand, we want our formalism to not be overly restrictive; that is, we want to accept those protocols that do not succumb to “feasible attacks”.

This chapter surveys a general methodology for defining security of cryptographic protocols. The methodology, often dubbed the “trusted party paradigm”, allows for defining the security requirements of practically any cryptographic task in a unified and natural way. We first review a basic formulation that captures security in isolation from other protocol instances. Next we address the secure composition problem, namely the vulnerabilities resulting from the interactions among different protocol instances that run alongside each other in the same system. We demonstrate the limitations of the basic formalism and review a formalism that guarantees security of protocols even in general composite systems.

This chapter overlaps the previous one in some of the material. There is however a difference in stress: The stress here is more on the definitional aspects and in particular on the challenge in capturing security properties of individual protocols within more complex environments.