Specifying distributed trust management in LolliMon

We propose the monadic linear logic programming language LolliMon as a new foundation for the specification of distributed trust management systems, particularly the RT framework. LolliMon possesses features that make it well-suited to this application, including rigorous logical foundations, an expressive formula language, strong typing, and saturation as a proof resolution strategy. We specify certificate chain discovery in full RT for authorization in a distributed environment where certificates may be stored nonlocally and selective retrieval is necessary. The uniform LolliMon specification of authorization and certificate chain discovery eases formal reasoning about the system, and scales to a rich collection of trust management features. The executable LolliMon specification also serves as a prototype implementation. Categories and Subject Descriptors C.2.0 [Computer Networks]: General—Security and protection General Terms Security, Languages, Theory Keywords Distributed...

• Type: Conference
• Year: 2006
• Where: PLDI
• Authors: Jeff Polakow, Christian Skalka
• Keywords: Certificate Chain Discovery, Keywords Distributed Authorization, PLDI 2006, Programming Languages, Trust Management