Evidential Authorization

Consider interaction of principals where each principal has its own policy and different principals may not trust each other. In one scenario the principals could be pharmaceutical companies, hospitals, biomedical labs and health related government institutions. In another scenario principals could be navy fleets of different and not necessarily friendly nations. In spite of the complexity of interaction, one may want to ensure that certain properties remain invariant. For example, in the navy scenario, each fleet should have enough information from other fleets to avoid unfortunate incidents. Furthermore, one wants to use automated provers to prove invariance. A natural approach to this and many other important problems is to provide a high-level logic-based language for the principals to communicate. We do just that. Three years ago two of us presented the first incarnation of Distributed Knowledge Authorization Language (DKAL). Here we present a new and much different incarnation of DKAL that we call Evidential DKAL. Statements communicated in Evidential DKAL are supposed to be accompanied with sufficient justifications. In general, we construe the term "authorization" in the acronym "DKAL" rather liberally; DKAL is essentially a general policy language. There is a wide spectrum of potential applications of DKAL. One ambitious goal is to provide a framework for establishing and maintaining invariants.