[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.
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
Language :
English
Title :
Model-based verification of a security protocol for conditional access to services
M. Abadi and A. Gordon, "A calculus for cryptographic protocols - The spi calculus," in Proc. of the 4th ACM Conference on Computer and Communications Security, 1997.
D. Bolignano, "Formal verification of cryptographic protocols," in Proc. of the 3rd ACM Conference on Computer and Communication Security, 1996.
D. Bolignano, "Towards a mechanization of cryptographic protocol verification," in Proc. of CAV 97, LNCS 1254, Springer-Verlag, 1997.
T. Bolognesi and E. Brinksma, "Introduction to the ISO specification language LOTOS," Computer Networks and ISDN Systems, Vol. 14, No. 1, pp. 25-59, 1987.
A. Bouajjani, J.-C. Fernandez, S. Graf, C. Rodriguez, and J. Sifakis, "Safety for branching time semantics," in 18th ICALP, Springer-Verlag, Berlin, July 1991.
M. Burrows, M. Abadi, and R. Needham, "A logic of authentication," ACM Transactions on Computer Systems, Vol. 8, 1990.
P. Chen and V Gligor, "On the formal specification and verification of a multiparty session protocol," in Proc. of the IEEE Symposium on Research in Security and Privacy, 1990.
D. Dolev, S. Even, and R. Karp, "On the security of ping-pong protocols," Information and Control, Vol. 55, pp. 57-68, 1982.
D. Dolev and A. Yao, "On the security of public key protocols," IEEE Transactions on Information Theory, Vol. 29, No. 2, pp. 198-208, March 1983.
H. Ehrig and B. Mahr, "Fundamentals of algebraic specification 1, equations and initial semantics," in W. Brauer, B. Rozenberg, and A. Salomaa (Eds.), EATCS, Monographs on Theoretical Computer Science, Springer Verlag, 1985.
J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu, "CADP (CÆSAR/ALDEBARAN development package): A protocol validation and verification toolbox," in R. Alur and T. Henzinger (Eds.), in Proc. of the 8th Conference on Computer-Aided Verification, New Brunswick, New Jersey, USA, Aug. 1996.
H. Garavel, "An overview of the eucalyptus toolbox, in Proc. of the COST247 Workshop," Maribor, Slovenia, June 1996.
F. Germeau and G. Leduc, "Model-based design and verification of security protocols using LOTOS," in Proc. of the DIMACS Workshop on Design and Formal Verification of Security Protocols, Rutgers University, NJ, USA, Sept. 1997.
F. Germeau and G. Leduc, "A computer-aided design of a secure registration protocol," Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE/PSTV'97, Chapman & Hall, London, pp. 145-160, 1997.
L. Guillou and J.-J. Quisquater, "A practical zero-knowledge protocol fitted to security microprocessor minimizing both transmission and memory," in Proc. of Eurocrypt'88, LNCS 330, Springer-Verlag, pp. 123-128.
J. Guimaraes, J.-M. Boucqueau, and B. Macq, "OKAPI: A Kernel for access control to multimedia services based on trusted third parties," in Proc. of ECMAST 96 - European Conference on Multimedia Applications, Services and Techniques, Louvain-la-Neuve, Belgium, pp. 783-798, May 1996.
ISO/IEC, Information Processing Systems - Open Systems Interconnection - LOTOS, a Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. IS 8807, Feb. 1989.
R. Kemmerer, "Using formal methods to analyse encryption protocols," IEEE Journal on Selected Areas in Communications, Vol. 7, No. 4, pp. 448-457, 1989.
R. Kemmerer, C. Meadows, and J. Millen, "Three systems for cryptographic protocol analysis," Journal of Cryptology, Vol. 7, No. 2, pp. 14-18, 1989.
S. Lacroix, J.-M. Boucqueau, J.-J. Quisquater, and B. Macq, "Providing equitable conditional access by use of trusted third parties," in Proc. of ECMAST 96 - European Conference on Multimedia Applications, Services and Techniques, Louvain-la-Neuve, Belgium, pp. 763-782, May 1996.
G. Leduc, O. Bonaventure, E. Koerner, L. Léonard, C. Pecheur, and D. Zanetti, "Specification and verification of a TTP protocol for the conditional access to services," in Proc. of 12th J. Cartier Workshop on Formal Methods and their Applications: Telecommunications, VLSI and Real-Time Computerized Control System, Montreal, Canada, Oct. 1996.
G. Lowe, "An attack on the Needham-Schroeder public-key authentication protocol," Information Processing Letters, Vol. 56, pp. 131-133, 1995.
G. Lowe, "Breaking and fixing the Needham-Schroeder public-key protocol using FDR," in T. Margaria and B. Steffen (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1055, Springer-Verlag, 1996.
C. Meadows, "Applying formal methods to the analysis of a key management protocol," Journal of Computer Security, 1992.
C. Meadows, "The NRL protocol analyser: An overview," Journal of Logic Programming, Vol. 26, No. 8, pp. 113-131, 1996.
C. Meadows, "Formal verification of cryptographic protocols: A survey," in Proc. of Asiacrypt 94, LNCS 917, pp. 133-150, 1995.
J. Millen, S. Clark, and S. Freedman, "The interrogator: Protocol security analysis," IEEE Transactions on Software Engineering, Vol. SE-13, No. 2, 1987.
R. Milner, Communication and Concurrency, Prentice-Hall Intern., London, 1989.
C. Pecheur, "Improving the specification of data types in LOTOS," Doctoral Dissertation, University of Liège, July 1996.
R. Rivest, A. Shamir, and L. Adleman, "On a method for obtaining digital signatures and public key cryptosystems," Communication of the ACM, Vol. 21, pp. 120-126, Feb. 1978.
B. Stepien, J. Tourrilhes, and J. Sincennes, "ELUDO: The University of Ottawa Toolkit," Technical Report, University of Ottawa, 1994. Obtainable by FTP at lotos.csi.uottawa.ca.
V Varadharajan, "Use of formal technique in the specification of authentication protocols," Computer Standards and Interfaces, Vol. 9, pp. 203-215, 1989.
T. Woo and S. Lam, "A semantic model for authentication protocols," in Proc. of IEEE Symposium on Research in Security and Privacy, 1993.
