Istituto di Informatica e Telematica     
Martinelli F., Matteucci I. An Approach for the Specification, Verification and Synthesis of Secure Systems. In: Electronic Notes Theoretical Computer Science, vol. 168 pp. 29 - 43. Elsevier Science Publishers, 2007.
In this paper we describe an approach based on open system analysis for the specification, verification and synthesis of secure systems. In particular, by using our framework, we are able to model a system with a possible intruder and verify whether the whole system is secure, i.e. whether the system satisfies a given temporal logic formula that describes its secure behavior. If necessary, we are also able to automatically synthesize a process that, by controlling the behavior of the possible intruder, enforces the desired secure behavior of the whole system.
DOI: 10.1016/j.entcs.2006.12.003
Subject open system analysis
partial model checking
secure systems analysis
K.6.5 Security and Protection (D.4.6, K.4.2)

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional