Information Technology Reference
In-Depth Information
security risks that include inappropriate disclosure of information, potential loss
and corruption of data, identity theft, and fraud. These security risks are rooted
in the inadequate verification of identity, authorization, and integrity.
To understand both the importance and the challenges of trustworthy sys-
tems in a global scale, consider the following scenario:
John Lee, an American tourist, is traveling in Asia on vacation twelve
time zones away from home. John has an accident and goes to a local
hospital for treatment. Dr. Gupta, the attending physician, concludes
that immediate intervention is required, but to provide safe and effective
treatment, she needs access to Mr. Lee's medical records located half-
way around the world. Dr. Gupta contacts her hospital's medical records
administrator, Mr. Kumar, to obtain access to Mr. Lee's records. Mr.
Kumar electronically retrieves Mr. Lee's medical records (and
only
his
medical records) from his doctor's computers within minutes, despite the
oce being closed.
In the above scenario, there are three primary concerns: (1) John Lee should
be assured that his private medical information is accessible only to the proper
authorities under specific circumstances and that the information is correct and
available when needed; (2) the hospital should be assured of immediate and
timely access in an emergency and that the information is correct; and (3) Mr.
Lee's doctor's oce should be free from liability concerns about the improper
release of records or incorrect data. These goals can be achieved by the cor-
rectness of access-control decisions and delegations. To assure the correctness
of access-control decisions, several components are required: a protocol for han-
dling brokered requests; consistent and predictable interpretations of requests;
and a logically sound theory for reasoning about delegations and access-control
decisions.
The specific protocol we consider in this paper is the Common Object Re-
quest Broker Architecture (CORBA) Common Secure Interoperability Version 2
Protocol (CSIv2). CORBA is an open standard that supports component-based
software designs and services at the middleware level [1]. CSIv2 is an accepted
CORBA standard in support of authentication of client identity [2]. The CSIv2
protocol was designed specifically to augment existing authentication technology
(e.g., SSL) with authorization and delegation information that can be used to
distinguish brokers from the clients who originate requests.
We focus on reasoning about access-control decisions and delegations related
to this protocol. We introduce a specialized modal logic that originally appeared
in a series of papers by Abadi and colleagues [5,3,8]. This logic supports reasoning
about the statements made by principals (i.e., the actors in a system), their
beliefs, their delegations, and their authorizations. To ensure the soundness of
the logic, we embedded this logic into the HOL system as a definitional extension
to verify the correctness of the formal definitions. A benefit provided by this
embedding is confidence in the correctness and soundness of the axioms of the
logic.
