To illustrate our method, this section presents an example of verification. We have chosen the registration part of the Equicrypt protocol, a conditional access protocol under design in the European ACTS OKAPI project [GBM96]. It allows a user to subscribe to multimedia services such as video on demand. The user must first register with a Trusted Third Party (TTP) using a challenge-response exchange. After a successful registration, this TTP issues a public-key certificate which allows the user to subscribe to a service offered by a service provider.
We concentrate on the verification of the registration protocol. This paper only presents an overview of the process. Complete details can be found in [GL97] for more interested readers.