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: http://labcom.inf.ufrgs.br/ceseg/anais/2005/artigos/12417.pdf or from the CADP Web site in PDF or PostScript |
Contact: | Luis Marco Cáceres Alvarez Laboratório de Redes e Gerência Universidade Federal de Santa Catarina Caixa Postal 476 Florianópolis SC Brazil Email: [email protected] |
Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |