|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