Reference : Model-based verification of a security protocol for conditional access to services
Scientific journals : Article
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/23849
Model-based verification of a security protocol for conditional access to services
English
Leduc, Guy mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques >]
Bonaventure, Olivier [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques > > > >]
Koerner, Eckhart [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques > > > >]
Léonard, Luc [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques > > > >]
Pecheur, Charles [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques > > > >]
Mar-1999
Formal Methods In System Design
14
2
171-191
Yes (verified by ORBi)
International
0925-9856
[en] 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.
Researchers
http://hdl.handle.net/2268/23849

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
RUN-PP99-01.pdfAuthor postprint257.04 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.