Distributed proving in access-control systems

We present a distributed algorithm for assembling a proof that a request satisfies an access-control policy expressed in a formal logic, in the tradition of Lampson et al. [16]. We show analytically that our distributed proof-generation algorithm succeeds in assembling a proof whenever a centralized prover utilizing remote certificate retrieval would do so. In addition, we show empirically that our algorithm outperforms centralized approaches in various measures of performance and usability, notably the number of remote requests and the number of user interruptions. We show that when combined with additional optimizations including caching and automatic tactic generation, which we introduce here, our algorithm retains its advantage, while achieving practical performance. Finally, we briefly describe the utilization of these algorithms as the basis for an access-control framework being deployed for use at our institution.