Specification and verification of a TTP protocol for the conditional access to services
Guy Leduc, Olivier Bonaventure, Eckhart Koerner, Luc Léonard, Charles Pecheur, David Zanetti · Open Repository and Bibliography (University of Liège) · 1996
In this paper we use the formal language LOTOS to specify the Equicrypt protocol and verify its robustness to attacks by an intruder. We use the model-based CADP verification tools from the Eucalyptus toolbox to discover some successful attacks against this protocol. 1. Introduction The Equicrypt protocol is a conditional access protocol under design in the European ACTS OKAPI project [GBM96]. It allows users to subscribe to multimedia services such as video on demand. Equicrypt is designed to be equitable, meaning that any user or service provider can potentially enter the system provided that it complies with this minimal protocol. This contrasts with proprietary systems which all use different conditional access protocols and thus oblige users to implement almost as many protocols as there are different service providers, which is a severe limitation. After a brief description of the protocol and its modelling in the formal language LOTOS [ISO 8807, BoB87], we will describe the ver...