Specification and Verification of Secure Business Transaction Systems

Abstract

Every organization has policies, defined either implicitly or explicitly, that are intended to influence the behavior ofsub jects and objects associated with the organization. A policy is a rule or a set ofcon straints that applies to some scenario in the daily life-cycle of the organization’s activity. Business rules describe terms and conditions, service provisions, contracts and their execution. Typically, a workflow specification in an organization is driven by business rules. On the other hand, security policies set restrictions on access to resources and regulate information flow. Security policies are domain-specific, restricting access to objects in that domain. A workflow specification may cut across different domains, requiring access to objects in different domains. The subjects involved in fulfilling the activities in a business workflow should have certain access rights to the objects in those domains, and should also be granted rights to let the information flow from one subject to another subject. There may exist a potential conflict between security and workflow policies. In this paper we provide a formal specification ofsecur ity policies, business policies, and workdlow schemes. The specification formalism naturally suggests a Hoare style axiomatic verification approach for detecting conflicts and proving security of business transactions.

This work is supported by a grant from Natural Sciences and Engineering Research Council, Canada.