[en] 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.
Disciplines :
Computer science
Author, co-author :
Leduc, Guy ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques
Bonaventure, Olivier; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques
Koerner, Eckhart; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques
Léonard, Luc; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques
Pecheur, Charles; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques
Zanetti, David; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore)
Language :
English
Title :
Specification and verification of a TTP protocol for the conditional access to services
Publication date :
October 1996
Event name :
12th J. Cartier Workshop on Formal Methods and their Applications
Event place :
Montréal, Canada
Event date :
Oct. 1996
Audience :
International
Main work title :
Formal Methods and their Applications: Telecommunications, VLSI and Real-Time Computerized Control Systems
