We define trust management systems as frameworks for authorization of non-local users of some resource over a network. Examples include KeyNote, SDSI/SPKI, and RT. Authorization decisions in these frameworks are often viewed as proofs of propositions involving the requestor and the resource, where certificates function as axioms. However, if proofs are complex, ideal security may need to be simplified for the sake of practical online authorization; nevertheless, it is desirable to be able to verify these simplifications offline, as a matter of course or if the need arises. We have recently developed a trust but verify (TbV) approach to trust management, where simplified online authorization decisions are required to have a formal relation with "ideal" authorization specifications, so that offline checking can be guaranteed to verify ideal security.
In a similar vein, we have extended the RT framework with an additive notion of risk, yielding the language RT^{R}. Risk is defined in an abstract manner, and can be wait-times, age of certificates, trustworthiness of the issuer, etc. We also define a certificate chain discovery algorithm that is directed, in the sense that it never attempts to retrieve certificate chains that overrun a given risk threshold.
On a more foundational level, we have been investigating the use of the LolliMon linear logic programming language for the specification and implementation of the RT framework. This solution is more scalable and easily verifiable than graph-theoretic approaches, and more applicable to certificate chain discovery problems than Datalog or Prolog.
This is joint work with Jeff Polakow, X. Sean Wang and Peter Chapin.