Non-interference through determinism

  • A. W. Roscoe
  • J. C. P. Woodcock
  • L. Wulf
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 875)


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.


Security Non-interference Formal methods Process algebra Determinism Automatic verification 


  1. [All91]
    P.G. Allen. “A comparison of non-interference and non-deducibility using CSP”, Proc. 1991 IEEE Computer Security Workshop, pp 43–54. IEEE Computer Society Press 1991.Google Scholar
  2. [BKS83]
    R-J. R. Back, R. Kurki-Suonio. “Decentralization of process nets with centralized control”, Proc 2nd Annual Symposium on Principles of Distributed Computing, Montreal, 1983.Google Scholar
  3. [Col94]
    R. Collinson. “Proving Critical Properties of Functional Specifications”, Proc FME'94 Symposium, Springer-Verlag LNCS, Barcelona, October 1994.Google Scholar
  4. [Gas88]
    M. Gasser. Building a Secure Computer System, Van Nostrand Reinhold, 1988.Google Scholar
  5. [Gra92]
    J. Graham-Cumming. The Formal Development of Secure Systems, Oxford University DPhil Thesis, 1992.Google Scholar
  6. [Hoa85]
    C. A. R. Hoare. Communicating Sequential Processes, Prentice Hall 1985.Google Scholar
  7. [Jac90]
    J. L. Jacob. “Specifying Security Properties”, in C. A. R. Hoare (ed), Developments in Concurrency and Communication, ACM Press, 1990.Google Scholar
  8. [Jon92]
    R. B. Jones. “Methods and Tools for the Verification of Critical Properties”, in C. B. Jones, R. C. Shaw, T. Denvir (eds) Proc 5th Refinement Workshop, Springer Verlag, London, 1992.Google Scholar
  9. [Ros93]
    A. W. Roscoe. “Unbounded Non-determinism in CSP”, Journal of Logic and Computation 3, 1993.Google Scholar
  10. [Ros94a]
    A. W. Roscoe. “Model Checking CSP”, in A. W. Roscoe (ed) A Classical Mind, Prentice Hall 1994.Google Scholar
  11. [Ros94b]
    A. W. Roscoe. “CSP and Determinism in Security Modelling”, in preparation.Google Scholar
  12. [RMacC94]
    A. W. Roscoe, H. MacCarthy. “Verifying a replicated database: A case study in model-checking CSP”, submitted for publication.Google Scholar
  13. [Rya91]
    P. Y. A. Ryan. “A CSPformulation of non-interference”, Cipher, pp 19–27. IEEE Computer Society Press, 1991.Google Scholar
  14. [Spi92]
    J.M. Spivey, The Z Notation: A Reference Manual (2nd ed.), Prentice-Hall International, 1992.Google Scholar
  15. [WM90]
    J. C. P. Woodcock, C. Morgan. “Refinement of State-based Concurrent Systems”, Proc VDM Symposium 1990, LNCS 428, Springer Verlag.Google Scholar
  16. [Woo94]
    J. C. P. Woodcock. “CSP Interpretations of Z Specifications”, in preparation.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • A. W. Roscoe
    • 1
  • J. C. P. Woodcock
    • 1
  • L. Wulf
    • 1
  1. 1.Oxford University Computing LaboratoryOxfordUK

Personalised recommendations