Database of Case Studies Achieved Using CADP

Multilateral and RBAC Security for Management of Distributed Systems

Organisation: Laboratório de Redes e Gerência, Universidade Federal de Santa Catarina (BRAZIL)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: System Security.

Period: 2005

Size: n/a

Description: Role-based access control (RBAC) is a mechanism for controlling access to files and other resources in a computer system by assigning roles to users, rather than assigning users with particular access rights or privileges. RBAC is increasingly used in complex distributed systems, because it reduces the complexity of user access management.

This case study concerns a real-time accounting system with multiple users and multiple suppliers, where both the Multilateral Security and RBAC models are applied. The system was specified in LOTOS and the CAESAR compiler of CADP was used to create the Labelled Transition System (LTS) of the specification in BCG format, for visual inspection and validation purposes. A prototype application was also developed.

Conclusions: This case study presents a typical workflow for using CADP to verify a LOTOS specification for an application that is relatively simple but of critical importance.

Publications: [Alvarez-Westphall-Westphall-05] Luis Marco Cáceres Alvarez, Carlos Becker Westphall, and Carla Merkle Westphall. "Segurança Multilateral e RBAC para Gerência de Contabilidade em Sistemas Distribuídos". V Simpósio Brasileiro em Segurança da Informação e de Sistemas Computacionais (Brazilian symposium on information and computer systems security), 216-230, 2005, in Portuguese.
Available on-line at:
or from the CADP Web site in PDF or PostScript
Luis Marco Cáceres Alvarez
Laboratório de Redes e Gerência
Universidade Federal de Santa Catarina
Caixa Postal 476

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Thu Feb 11 12:22:05 2021.

Back to the CADP case studies page