loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
The Eighth IEEE Computer Security Foundations Workshop (CSFW '95)
The security checker: a semantics-based tool for the verification of security properties
Kenmare, County Kerry, Ireland
March 13-March 15
ISBN: 0-8186-7033-9
ASCII Text
x 
 
R. Focardi, R. Gorrieri, V. Panini, "The security checker: a semantics-based tool for the verification of security properties," Computer Security Foundations Workshop, IEEE, pp. 60, The Eighth IEEE Computer Security Foundations Workshop (CSFW '95), 1995.
 
 
BibTex
x
 
@article{ 10.1109/CSFW.1995.518553,
author = {R. Focardi and R. Gorrieri and V. Panini},
title = {The security checker: a semantics-based tool for the verification of security properties},
journal ={Computer Security Foundations Workshop, IEEE},
volume = {0},
year = {1995},
issn = {1063-6900},
pages = {60},
doi = {http://doi.ieeecomputersociety.org/10.1109/CSFW.1995.518553},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computer Security Foundations Workshop, IEEE
TI - The security checker: a semantics-based tool for the verification of security properties
SN - 1063-6900
SP
EP
A1 - R. Focardi,
A1 - R. Gorrieri,
A1 - V. Panini,
PY - 1995
KW - security of data; formal verification; formal specification; process algebra; security checker; semantics-based tool; security properties verification; automatic verification; specifications; security process algebra; confidentiality; concurrency workbench
VL - 0
JA - Computer Security Foundations Workshop, IEEE
ER -
 
R. Focardi, Dipartimento di Sci. dell'Inf., Bologna Univ., Italy
R. Gorrieri, Dipartimento di Sci. dell'Inf., Bologna Univ., Italy
V. Panini, Dipartimento di Sci. dell'Inf., Bologna Univ., Italy
The security checker (SC for short) is a semantic tool for the automatic verification of some information flow properties. The specifications given as inputs to SC are terms of the security process algebra (SPA for short), a language suited for the specification of systems where actions belong to two different levels of confidentiality. The information flow security properties which can be verified by SC are some of those classified in previous papers. They are derivations of some classic notions, e.g. non interference. The tool is based on the same architecture of the concurrency workbench, from which some modules have been integrally imported. The usefulness of the tool is tested with the significative case-study of an access monitor.
Index Terms:
security of data; formal verification; formal specification; process algebra; security checker; semantics-based tool; security properties verification; automatic verification; specifications; security process algebra; confidentiality; concurrency workbench
Citation:
R. Focardi, R. Gorrieri, V. Panini, "The security checker: a semantics-based tool for the verification of security properties," csfw, pp.60, The Eighth IEEE Computer Security Foundations Workshop (CSFW '95), 1995
Usage of this product signifies your acceptance of the Terms of Use.