Formalization and Proof of Secrecy Properties; Workshop summary

摘要

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 are 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 wider 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 were 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. Below are some specific questions that were asked of each of the panelists.