Formalization and Proof of Secrecy Properties
MetadataShow full item record
After looking at the security literature, you will find secrecy is formalized in different ways, depending on the application. Applications have threat models that influence our choice of secrecy properties. A property may be reasonable in one context and completely unsatisfactory in another if other threats exist. The primary goal of this panel is to foster discussion on what sorts of secrecy properties arc appropriate for different applications and to investigate what they have in common. We also want to explore what is meant by secrecy in different contexts. Perhaps there is enough overlap among our threat models that we can begin to identify some key secrecy properties for 'vidcr application. Currently, secrecy is treated in rather ad hoc ways. With some agreement among calculi for expressing protocols and systems, we might even be able to use one another's proof techniques for proving secrecy! Four experts \Vere invited as panelists. Two panelists, Riccardo Focardi and Martin Abadi, represent formalizations of secrecy as demanded by secure systems that aim to prohibit various channels, or insecure information flows. More specifically, they represent noninterference-based secrecy. The other two panelists, Cathy Meadows and Jon Millen, represent formalizations of secrecy for protocols based on the Dolev-Yao threat model.
RightsThis publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.
Showing items related by title, author, creator and subject.
Volpano, Dennis (1999-09);Safety and secrecy are formulated for a deterministic programming language. A safety property is defined as a set of program traces and secrecy is defined as a binary relation on traces, characterizing a form of Noninterference. ...
Falby, Naomi; Thompson, Michael F.; Irvine, Cynthia E. (IEEE, 2004-06-00);The Center for the Information Systems Studies and Research (CISR) at the Naval Postgraduate School has established a broad program in computer and network security education. The program, founded on a core in traditional ...
Center on Contemporary Conflict; Long, Austin (Monterey, California: Naval Postgraduate School, 2016-10);Clandestine capabilities are an increasingly relevant part of nuclear strength, and will likely be a key determinant of deterrence success and strategic stability in future world politics. While the challenge of managing ...