Model-Based Verification of a Security Protocol for the Conditional Access to Services

Fri, 06/22/2007 - 23:20 by Olivier Bonaventure • Categories:

Abstract

We use the formal language LOTOS to specify and verify the robustness of the Equicrypt protocol under design in the European OKAPI project for conditional access to multimedia services. We state some desired security properties and formalize them. We describe a generic intruder process and its modelling, and show that some properties are falsified in the presence of this intruder. The diagnostic sequences can be used almost directly to exhibit the scenarios of possible attacks on the protocol. Finally, we propose an improvement of the protocol which satisfies our properties.

Authors
G. Leduc, O. Bonaventure, E. Koerner, L. Léonard and C. Pecheur
Source
Formal Methods in System Design, 14(2), March 1999.
Full text
pdf   (391.99 KB)
Cite it
BibTex
Copyright
See here

IEEE Copyright Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

ACM Copyright Notice: Copyright 1999 by the Association for Computing Machinery, Inc. Permission to make digital or hard copies of part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page or intial screen of the document. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept., ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org.

Springer-Verlag LNCS Copyright Notice: The copyright of these contributions has been transferred to Springer-Verlag Berlin Heidelberg New York. The copyright transfer covers the exclusive right to reproduce and distribute the contribution, including reprints, translations, photographic reproductions, microform, electronic form (offline, online), or any other reproductions of similar nature. Online available from Springer-Verlag LNCS series.