Chris Skalka
Department of
Computer Science
The University of Vermont
Date:
Time:
Location:
367 Votey
Abstract
Trust management systems allow decentralized authorization of security critical actions in modern distributed systems. Examples include SDSI/SPKI, KeyNote, and RT. A variety of logics have been used to specify the semantics of trust management systems, being sufficiently expressive to capture their meaning in a natural manner, and providing them with rigorous mathematical foundations. We propose LolliMon, a linear logic programming language, as a new foundation for RT trust management, since it possesses unique features allowing a simple and scalable implementation of the system that is easily proven correct. In particular, conditional subgoals, linear hypotheses, and a mix of bottom-up and top-down proof strategies, allow for a seamless integration of authorization steps and non-local certificate retrieval, commonly called certificate chain discovery. This technique is easily adapted to a variety of enhancements of the basic system. Furthermore, we show how strategies for minimizing the cost of certificate retrieval can be encoded in the logical specification, providing efficiency without compromising mathematical rigor for security.
This is joint work with Peter Chapin (UVM), X. Sean Wang (UVM), and
Jeff Polakow (AIST, CVS, JST).