Skip to main content

Technical Reports: CMU-CyLab-08-003

Title:Towards a Theory of Secure Systems
Authors:Deepak Garg, Jason Franklin, Dilsun Kaynar, Anupam Datta
Publication Date:February 4, 2008


We initiate a program to develop a principled theory of secure systems. Our main technical result is a formal logic for reasoning about a network of shared memory, multi-user systems. The logic is inspired by an existing logic for security protocols. It extends the attacker model and adds shared memory, time, and limited forms of access control. We prove soundness for the proof system in the presence of an attacker who controls the network and has partial control over shared memory on individualmachines. We illustrate the use of the logic by proving a relevant security property of a part of the Trusted Computing Group’s remote attestation protocol.

Full Report: CMU-CyLab-08-003