Specification and verification of workflows with RBAC mechanism and SoD constraints

Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi

Research output: Contribution to journalArticle

8 Citations (Scopus)

Abstract

Security considerations, such as role-based access control (RBAC) mechanism and separation of duty (SoD) constraints, are important and integral to workflow systems. Since the definition of workflows with these security considerations is a complicated and error-prone process, rigorous verification techniques are desirable for uncovering logical errors and assuring correctness. We propose the use of an equation-based method - the OTS/Cafe OBJ method to model, specify and verify workflows with such security considerations. Specifically, a workflow with the security considerations, is modeled as an OTS, a kind of transition system; the OTS is then specified in CafeOBJ, an algebraic specification language. We verify that the OTS has desired safety and liveness properties by using the CafeOBJ system as an interactive theorem prover. A case study on a sample workflow that deals with travel expense reimbursement is used to demonstrate our method.

Original languageEnglish
Pages (from-to)3-32
Number of pages30
JournalInternational Journal of Software Engineering and Knowledge Engineering
Volume17
Issue number1
DOIs
Publication statusPublished - Feb 1 2007

Fingerprint

Access control
Specifications
Specification languages

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Networks and Communications
  • Computer Graphics and Computer-Aided Design
  • Artificial Intelligence

Cite this

Specification and verification of workflows with RBAC mechanism and SoD constraints. / Kong, Weiqiang; Ogata, Kazuhiro; Futatsugi, Kokichi.

In: International Journal of Software Engineering and Knowledge Engineering, Vol. 17, No. 1, 01.02.2007, p. 3-32.

Research output: Contribution to journalArticle

@article{c0b26419976e4d1baf5a410166ce2575,
title = "Specification and verification of workflows with RBAC mechanism and SoD constraints",
abstract = "Security considerations, such as role-based access control (RBAC) mechanism and separation of duty (SoD) constraints, are important and integral to workflow systems. Since the definition of workflows with these security considerations is a complicated and error-prone process, rigorous verification techniques are desirable for uncovering logical errors and assuring correctness. We propose the use of an equation-based method - the OTS/Cafe OBJ method to model, specify and verify workflows with such security considerations. Specifically, a workflow with the security considerations, is modeled as an OTS, a kind of transition system; the OTS is then specified in CafeOBJ, an algebraic specification language. We verify that the OTS has desired safety and liveness properties by using the CafeOBJ system as an interactive theorem prover. A case study on a sample workflow that deals with travel expense reimbursement is used to demonstrate our method.",
author = "Weiqiang Kong and Kazuhiro Ogata and Kokichi Futatsugi",
year = "2007",
month = "2",
day = "1",
doi = "10.1142/S0218194007003124",
language = "English",
volume = "17",
pages = "3--32",
journal = "International Journal of Software Engineering and Knowledge Engineering",
issn = "0218-1940",
publisher = "World Scientific Publishing Co. Pte Ltd",
number = "1",

}

TY - JOUR

T1 - Specification and verification of workflows with RBAC mechanism and SoD constraints

AU - Kong, Weiqiang

AU - Ogata, Kazuhiro

AU - Futatsugi, Kokichi

PY - 2007/2/1

Y1 - 2007/2/1

N2 - Security considerations, such as role-based access control (RBAC) mechanism and separation of duty (SoD) constraints, are important and integral to workflow systems. Since the definition of workflows with these security considerations is a complicated and error-prone process, rigorous verification techniques are desirable for uncovering logical errors and assuring correctness. We propose the use of an equation-based method - the OTS/Cafe OBJ method to model, specify and verify workflows with such security considerations. Specifically, a workflow with the security considerations, is modeled as an OTS, a kind of transition system; the OTS is then specified in CafeOBJ, an algebraic specification language. We verify that the OTS has desired safety and liveness properties by using the CafeOBJ system as an interactive theorem prover. A case study on a sample workflow that deals with travel expense reimbursement is used to demonstrate our method.

AB - Security considerations, such as role-based access control (RBAC) mechanism and separation of duty (SoD) constraints, are important and integral to workflow systems. Since the definition of workflows with these security considerations is a complicated and error-prone process, rigorous verification techniques are desirable for uncovering logical errors and assuring correctness. We propose the use of an equation-based method - the OTS/Cafe OBJ method to model, specify and verify workflows with such security considerations. Specifically, a workflow with the security considerations, is modeled as an OTS, a kind of transition system; the OTS is then specified in CafeOBJ, an algebraic specification language. We verify that the OTS has desired safety and liveness properties by using the CafeOBJ system as an interactive theorem prover. A case study on a sample workflow that deals with travel expense reimbursement is used to demonstrate our method.

UR - http://www.scopus.com/inward/record.url?scp=33947671905&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33947671905&partnerID=8YFLogxK

U2 - 10.1142/S0218194007003124

DO - 10.1142/S0218194007003124

M3 - Article

AN - SCOPUS:33947671905

VL - 17

SP - 3

EP - 32

JO - International Journal of Software Engineering and Knowledge Engineering

JF - International Journal of Software Engineering and Knowledge Engineering

SN - 0218-1940

IS - 1

ER -