SSCC (Security System against the Cloning of Cellular phones).

Organisation:	Federal University of Santa Catarina at Florianopolis (BRAZIL)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Security.
Period:	1999.
Size:	n/a
Description:	Security has become an important area in the field of network management. A security management service is responsible for providing a safe environment for both the operation and management of resources in a domain. The security system proposed, called SSCC, aims at increasing security in telecommunication networks by avoiding frauds due to cloned mobile phones (i.e., having both the number and series of a genuine phone). An abstract specification of the SSCC system, corresponding to a formalization of the user requirements of SSCC, has been developed in LOTOS. Then, this specification has been refined in several steps by defining the structure and behaviour of its various components: the manager (which is responsible for receiving notifications and sending alarms to the users) and the set of managed sites (each of them consisting of a management agent, a reference baseline, and a file recording the telephone calls). The CADP toolset has been employed for two purposes. Firstly, CAESAR and ALDEBARAN have been used to formally verify the correctness of the refinements, by generating the labelled transition systems (LTSs) of two successive refinements and compring them modulo observational equivalence. Secondly, CAESAR has been used to generate C code from the refined LOTOS specification. This allowed both to establish the correctness of the LOTOS specification of SSCC (w.r.t. the initial abstract specification) and to have a prototype of the system in C. This C code has been helpful later for developing the C++ and JAVA final implementation of the SSCC system.
Conclusions:	The model-checking techniques employed have been very useful for this case-study. LOTOS allows a rigorous specification and validation process, and the CADP toolset provides verification and code generation facilities that make the development reliable and faster.
Publications:	[Notare-Cruz-Riso-Westphall-99] M. S. M. A. Notare, F. A. S. Cruz, B. G. Riso, and C. B. Westphall. "Wireless Communications: Security Management Against Cloned Cellular Phones". Proceedings of the IEEE Wireless Communications and Networking Conference WCNC'99 (New Orleans, LA, USA), September 1999. Available online from the CADP Web site in PDF or PostScript [Notare-Boukerche-Cruz-Riso-Westphall-99] M. S. M. A. Notare, A. Boukerche, F. A. S. Cruz, B. G. Riso, and C. B. Westphall. "Security Management against Cloning Mobile Phones". Proceedings of IEEE GLOBECOM'99 (Rio de Janeiro, RJ, Brazil), December 1999. Available online from the CADP Web site in PDF or PostScript
Contact:	Mirella Sechi Moretti Annoni Notare Universidade Federal de Santa Catarina - UFSC Centro Tecnologico - CTC Laboratorio de Redes e Gerencia - LRG Caixa Postal 476 88040-970 Florianopolis, SC - Brazil E-mail: mirela@fastlane.com.br
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page