Abstract
We propose a general framework of secrecy and preservation of secrecy for labeled transition systems. Our definition of secrecy is parameterized by the distinguishing power of the observer, the properties to be kept secret, and the executions of interest, and captures a multitude of definitions in the literature. We define a notion of secrecy preserving refinement between systems by strengthening the classical trace-based refinement so that the implementation leaks a secret only when the specification also leaks it. We show that secrecy is in general not definable in μ-calculus, and thus not expressible in specification logics supported by standard model-checkers. However, we develop a simulation-based proof technique for establishing secrecy preserving refinement. This result shows how existing refinement checkers can be used to show correctness of an implementation with respect to a specification.
This research was partially supported by NSF Cybertrust award CNS 0524059.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abadi, M.: Protection in programming-language translations. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 868–883. Springer, Heidelberg (1998)
Alur, R., Henzinger, T.A., Mang, F., Qadeer, S., Rajamani, S., Tasiran, S.: MOCHA: Modularity in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)
Barthe, G., D’Argenio, P., Rezk, T.: Secure Information Flow by Self-Composition. In: Proc. of CSFW 2004, pp. 100–114 (2004)
: A Theorem Proving Approach to Analysis of Secure Information Flow. In: Proc. of SPC 2005, pp. 193–208 (2005)
Halpern, J., O’Neill, K.: Secrecy in multiagent systems. In: Proc. of CSFW 2002, pp. 32–46 (2002)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Jürjens, J.: Secrecy-preserving refinement. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 135–152. Springer, Heidelberg (2001)
Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16(3), 872–923 (1994)
Mantel, H.: Preserving information flow properties under refinement. In: Proc. of SP 2001, pp. 78–91 (2001)
McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proc. of SP 1994, pp. 79–93 (1994)
McMillan, K.L.: A compositional rule for hardware design refinement. In: CAV 1997, pp. 24–35 (1997)
Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: CADE 1992, pp. 748–752 (1992)
Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)
Schneider, F.B. (ed.): Trust in Cyberspace. National Academy Press (1999)
Terauchi, T., Aiken, A.: Secure Information Flow as a Safety Problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352–367. Springer, Heidelberg (2005)
Zakinthinos, A., Lee, E.S.: A general theory of security properties. In: Proc. of SP 1997, pp. 94–102 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alur, R., Černý, P., Zdancewic, S. (2006). Preserving Secrecy Under Refinement. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds) Automata, Languages and Programming. ICALP 2006. Lecture Notes in Computer Science, vol 4052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11787006_10
Download citation
DOI: https://doi.org/10.1007/11787006_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-35907-4
Online ISBN: 978-3-540-35908-1
eBook Packages: Computer ScienceComputer Science (R0)