A useful paradigm of system development is that of step-wise refinement. In contrast to other system properties, many security properties proposed in the literature are not preserved under refinement (refinement paradox). We present work towards a framework for stepwise development of secure systems by showing a notion of secrecy (that follows a standard approach) to be preserved by standard refinement operators in the specification framework Focus (extended with cryptographic primitives). We also give a rely/guarantee version of the secrecy property and show preservation by refinement. We use the secrecy property to uncover a previously unpublished flaw in a proposed variant of TLS, propose a correction and prove it secure. We give an abstract specification of a secure channel satisfying secrecy and refine it to a more concrete specification that by the preservation result thus also satisfies secrecy. © Springer-Verlag Berlin Heidelberg 2001.
CITATION STYLE
Jürjens, J. (2001). Secrecy-preserving refinement. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2021 LNCS, pp. 135–152). Springer Verlag. https://doi.org/10.1007/3-540-45251-6_8
Mendeley helps you to discover research relevant for your work.