Computer Security and CryptographyReading Group
February 2004 List

URL: http://doi.acm.org/10.1145/363516.363528

Due to the rapid growth of Internet the World Wide Web has become a very important concern in the design and implementation of software systems. Since security has become an important issue, the number of protocols in this domain has become very large. These protocols are very diverse in nature. If a software architect wants to deploy some of these protocols in a system, they have to be sure that the protocol has the right properties as dictated by the requirements of the system. In this article we present BRUTUS, a tool for verifying properties of security protocols. This tool can be viewed as a special-purpose model checker for security protocols. We also present reduction techniques that make the tool efficient. Experimental results are provided to demonstrate the efficiency of BRUTUS.

URL: http://doi.acm.org/10.1145/360303.360333

A model of protection mechanisms in computing systems is presented and its appropriateness is argued. The "safety" problem for protection systems under this model is to determine in a given situation whether a subject can acquire a particular right to an object. In restricted cases, it can be shown that this problem is decidable, i.e. there is an algorithm to determine whether a system in a particular configuration is safe. In general, and under surprisingly weak assumptions, it cannot be decided if a situation is safe. Various implications of this fact are discussed.

URL: http://www.cs.wisc.edu/~mihai/_/JonesLiptonSnyder1976.pdf

URL: http://citeseer.nj.nec.com/weeks01understanding.html

This paper presents a mathematical framework for expressing trust management systems. The framework makes it easier to understand existing systems and to compare them to one another, as well as to design new systems. The framework defines the semantics of a trust management engine via a least fixpoint in a lattice, which, in some situations, leads to an efficient implementation. To demonstrate its flexibility, we present KeyNote and SPKI as instantiations of the framework.