next up previous
Next: The registration protocol Up: Verification using LOTOS Previous: The verification

An example of verification


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.