Preserving secrecy under refinement
Alur R, Cerny P, Zdancewic S. 2006. Preserving secrecy under refinement. 33rd International Colloquium on Automata, Languages and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 4052, 107–118.
Download
No fulltext has been uploaded. References only!
Conference Paper
| Published
| English
Scopus indexed
Author
Alur, Rajeev;
Cerny, PavolISTA;
Zdancewic, Steve
Series Title
LNCS
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.
Publishing Year
Date Published
2006-01-01
Proceedings Title
33rd International Colloquium on Automata, Languages and Programming
Publisher
Springer
Volume
4052
Page
107 - 118
Conference
ICALP: Automata, Languages and Programming
IST-REx-ID
Cite this
Alur R, Cerny P, Zdancewic S. Preserving secrecy under refinement. In: 33rd International Colloquium on Automata, Languages and Programming. Vol 4052. Springer; 2006:107-118. doi:10.1007/11787006_10
Alur, R., Cerny, P., & Zdancewic, S. (2006). Preserving secrecy under refinement. In 33rd International Colloquium on Automata, Languages and Programming (Vol. 4052, pp. 107–118). Springer. https://doi.org/10.1007/11787006_10
Alur, Rajeev, Pavol Cerny, and Steve Zdancewic. “Preserving Secrecy under Refinement.” In 33rd International Colloquium on Automata, Languages and Programming, 4052:107–18. Springer, 2006. https://doi.org/10.1007/11787006_10.
R. Alur, P. Cerny, and S. Zdancewic, “Preserving secrecy under refinement,” in 33rd International Colloquium on Automata, Languages and Programming, 2006, vol. 4052, pp. 107–118.
Alur R, Cerny P, Zdancewic S. 2006. Preserving secrecy under refinement. 33rd International Colloquium on Automata, Languages and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 4052, 107–118.
Alur, Rajeev, et al. “Preserving Secrecy under Refinement.” 33rd International Colloquium on Automata, Languages and Programming, vol. 4052, Springer, 2006, pp. 107–18, doi:10.1007/11787006_10.