Reference from ESORICS proceedings

Third European Symposium on Research in Computer Security (ESORICS 94)

Non-interference through Determinism

A.W. Roscoe, J.C.P. Woodcock, L. Wulf

Keywords : security, non-interference, formal methods, process algebra, determinism, automatic verification

Abstract : The standard approach to the specification of a secure system is to present a (usually state-based) abstract security model separately from the specification of the system's functional requirements, and establishing a correspondence between the two specifications. This complex treatment has resulted in development methods distinct from those usually advocated for general applications. We provide a novel and intellectually satisfying formulation of security properties in a process algebraic framework, and show that these are preserved under refinement. We relate the results to a more familiar state-based (Z) specification methodology. There are efficient algorithms for verifying our security properties using model checking.

(Pages 3-18)

Proceedings table of contents