Preserving Security Properties under Refinement

Abstract : Communication is one of the cornerstone of our everyday life. Guar- anteeing the security of a communication is a very important chal- lenge. In this paper, we propose a formal top-down approach for assuring that security properties are preserved during the develop- ment of a complex and concurrent system, i.e., within passage from specification to implementation of the components of the system. Indeed, we investigate on the set of requirements a refinement function has to satisfy for preserving a class of properties that can be formalized as specific instances of a general scheme, called Generalized Non Deducibility on Composition (GNDC). Hence, we show that it is possible to guarantee that the refinement of a considered system that is verified to be GNDC at a high level of abstraction, is GNDC also at a lower one without checking it again.
Type de document :
Communication dans un congrès
ICSE, May 2011, Waikiki, Honolulu, HI,, United States. 2011
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger
Contributeur : Ilaria Matteucci <>
Soumis le : vendredi 20 janvier 2012 - 11:27:00
Dernière modification le : vendredi 27 janvier 2012 - 09:55:05
Document(s) archivé(s) le : samedi 21 avril 2012 - 02:25:45


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-00661621, version 1



Fabio Martinelli, Ilaria Matteucci. Preserving Security Properties under Refinement. ICSE, May 2011, Waikiki, Honolulu, HI,, United States. 2011. 〈hal-00661621〉



Consultations de la notice


Téléchargements de fichiers