Team for Research in
Ubiquitous Secure Technology

Citation
Deepak Garg, Jason Franklin, Dilsun Kaynar, Anupam Datta. "A Logic for Reasoning about Networked Secure Systems". Joint Workshop FCS-ARSPA-WITS, 2008.

Abstract
We initiate a program to model and analyze end-to-end security properties of contemporary secure systems that rely on network protocols and memory protection. Specifically, this paper introduces the Logic of Secure Systems (LS2). LS2 extends an existing logic for security protocols by incorporating shared memory, time and limited forms of access control. The proof system for LS2 supports highlevel reasoning about secure systems in the presence of adversaries on the network and the local machine. We prove a soundness theorem for the proof system and illustrate its use by proving a relevant security property of a protocol inspired by the Transport Layer Protocol of the Secure Shell (SSH).

Electronic downloads

• http://www.andrew.cmu.edu/user/danupam/gfkd-fcs08.pdf

• HTML

  Deepak Garg, Jason Franklin, Dilsun Kaynar, Anupam Datta.
  <a href="http://www.truststc.org/pubs/412.html"
  >A Logic for Reasoning about Networked Secure
  Systems</a>, Joint Workshop FCS-ARSPA-WITS, 2008.

• Plain text

  Deepak Garg, Jason Franklin, Dilsun Kaynar, Anupam Datta.
  "A Logic for Reasoning about Networked Secure
  Systems". Joint Workshop FCS-ARSPA-WITS, 2008.

• BibTeX

  @inproceedings{GargFranklinKaynarDatta08_LogicForReasoningAboutNetworkedSecureSystems,
      author = {Deepak Garg and Jason Franklin and Dilsun Kaynar
                and Anupam Datta},
      title = {A Logic for Reasoning about Networked Secure
                Systems},
      booktitle = {Joint Workshop FCS-ARSPA-WITS},
      year = {2008},
      abstract = {We initiate a program to model and analyze
                end-to-end security properties of contemporary
                secure systems that rely on network protocols and
                memory protection. Specifically, this paper
                introduces the Logic of Secure Systems (LS2). LS2
                extends an existing logic for security protocols
                by incorporating shared memory, time and limited
                forms of access control. The proof system for LS2
                supports highlevel reasoning about secure systems
                in the presence of adversaries on the network and
                the local machine. We prove a soundness theorem
                for the proof system and illustrate its use by
                proving a relevant security property of a protocol
                inspired by the Transport Layer Protocol of the
                Secure Shell (SSH).},
      URL = {http://www.truststc.org/pubs/412.html}
  }
  

Posted by Anupam Datta on 25 Jul 2008.
For additional information, see the Publications FAQ or contact webmaster at www truststc org.