This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Specification and Validation of a Security Policy Model
February 1995 (vol. 21 no. 2)
pp. 63-68
This paper describes the development of a formal security policy model in Z for the NATO Air Command and Control System (ACCS): a large, distributed, multilevel-secure system. The model was subject to manual validation, and some of the issues and lessons in both writing and validating the model are discussed.

[1] R. Barden, S. Stepney, and D. Cooper,“The use of Z,”Z User Workshop,York, 1991, J. Nicholls, Ed. New York: Springer-Verlag, 1992.
[2] D. E. Bell and L. J. LaPadula,“Secure computer system: Unified exposition and multics interpretation,”MTR-2997, Revision 1, Mar. 1976.
[3] D. D. Clark and D. R. Wilson,“A comparison of commercial and military computer security policies,”inProc. IEEE Symposium on Security and Privacy,1987.
[4] M. Flynn, T. Hoverd, and D. Brazier,“Formaliser—An interactive support tool for Z,”inZ User Workshop,Oxford, 1989, J. Nicholls, Ed. New York: Springer-Verlag, 1989.
[5] L. Semmens and P. Allen,“Using Yourdon and Z: An approach to formal specification,”inZ User Workshop,Oxford, 1990, J. E. Nicholls, Ed. New York: Springer-Verlag, 1991.
[6] F. Polack, M. Whiston, and P. Hitchcock,“Structured analysis—A draft method for writing Z specifications,”inZ User Workshop,York, 1991, J. Nicholls, Ed. New York: Springer-Verlag, 1992.
[7] S. Stepney,“Entity relationship diagrams and Z—The best of both worlds,”Logica Advanced Software Engi. Div., Tech. Rep. 3, 1991.
[8] D. A. Penny, R. C. Holt, and M. W. Godfrey,“Formal specification in metamorphic programming,”inVDM '91, 4th Int. Symp. VDM Europe Proc.New York: Springer-Verlag, 1991.
[9] D. Garlan and N. Delisle,“Formal specifications as reusable frameworks,”inVDM '90, 3rd Int. Symp. VDM Europe Proc.New York: Springer-Verlag, 1990.

Index Terms:
Security, security policy model, formal specification, Z, modeling, validation
Citation:
Anthony Boswell, "Specification and Validation of a Security Policy Model," IEEE Transactions on Software Engineering, vol. 21, no. 2, pp. 63-68, Feb. 1995, doi:10.1109/32.345822
Usage of this product signifies your acceptance of the Terms of Use.