Guttman (Ph.D. in philosophy (logic) at University of Chicago, BA in philosophy at Princeton) is Principal Scientist and Section Leader (Information Security Theory and Applications) at MITRE Corp. (Bedford, MA).

In these lectures we will explore formalisms for representing security. goals suited to specific problems of secure networked systems. Unlike non-interference, which provides a general framework for expressing security goals, these formalisms are tailored to particular problems, thus leading to easier proof methods and in some cases to efficient algorithms. We focus on two examples. First, packet trajectory security goals may be used to represent policies for distributed firewalls and for IP security. They lead to algorithms to design or validate secure distributed configurations. Second, constraints on bundles of strands represent confidentiality and authentication properties of cryptographic protocols. These properties and some more general characteristics of protocols can be proved using the bundle representation. The overall emphasis of these lectures will be on how to formulate security goals so that domain-specific rigorous methods can be applied to them.