Logical Foundations of Computer Security

The first of my four lectures on the logical foundations of computer security will establish the ma-thematical setting in which we will work, namely computational type theory. In this setting we can pursue algorithmic ideas from their natural expression in computer science articles to their codifi-cation in executable systems and finally to their incorporation into formal arguments that a system achieves some stated purpose. For this lecture we draw on material produced in previous summer school lectures, in particular on the booklet Naive Computational Type Theory from Marktoberdorf 2001. Another modern source of this material is the recent monograph by M. Sorensen and P. Ur-zyczyn, see [7]. The Nuprl version of computational type theory is presented in the article by Allen, Bickford et. al, see [2]. The second lecture will present an abstract theory of events which my colleague Mark Bickford and I created in 2003 for specifying distributed computing problems. This theory has been implemented in the Nuprl version of Computational Type Theory (CTT) by Mark. The theory is based on the causal order relation used by Leslie Lamport in this early work on the foundations of distributed computing. One good reference for this material are the MOD05 lectures notes by Mark Bickford and me, see [4]. The material was also presented in the introduction to the paper [5]