Formalization and Proof of Secrecy Properties
Loading...
Authors
Volpano, Dennis
Subjects
Advisors
Date of Issue
1999-06
Date
June 1999
Publisher
Language
Abstract
Type
Description
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.
Series/Report No
Department
Computer Science (CS)
Organization
Identifiers
NPS Report Number
Sponsors
Funder
Format
Citation
Proc. 12th IEEE Computer Security Foundations Workshop, pp. 92-95, Mordano Italy, June 1999.
Distribution Statement
Rights
This 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.