商务安全策略及其形式分析研究
|
摘要
安全策略和安全策略模型是开发安全产品和构建安全系统的基础和前提。基于Clark-Wilson完整性安全策略的商务安全策略是一种适用于商务环境的安全系统构建策略。和以机密性为特征的军事安全策略的研究深度和应用广度相比,以完整性为特征的商务安全策略的研究和应用都处于一个相对原始的阶段,这主要是由于对商务安全策略的应用场景和策略本身的认识不足所致,因此有必要对商务安全策略进行深入的研究。
商务安全策略研究的主要内容包括:安全策略制模和形式分析原理、商务安全策略框架模型研究以及形式分析。围绕着商务安全策略的制模和形式分析,本文取得了以下几个方面的成果:
第一:首次从安全策略应用场景的角度出发,把安全策略分为安全产品开发策略和安全系统构建策略,经研究发现策略应用场景是精确理解安全策略的一个关键因素,也是妨碍对以Clark-Wilson完整性安全策略为代表的商务安全策略进行制模和推广使用的主要原因之一。
第二:深入讨论了安全模型开发的方方面面,并且提出了一个实用的、易操作的、具有相当理论基础的安全策略制模方法。
第三:针对商务安全的本质就是对系统中的应用进行有效控制的指导思想,提出了一个商务安全策略的形式框架,首次完整地对Clark-Wilson完整性安全策略进行了形式制模,该框架具有扩展性好、兼容性高等方面的优势。
第四:提出了一个新颖的、可以依据系统所实现的策略进行安全监视的多策略安全监视框架。该框架可以很好地解决传统审计中的数据冗余过大和系统异常侦测时延过长的问题。
第五:针对当前形式开发中所存在的安全策略模型到安全功能规范之间的平滑过渡问题,本文直接把安全功能规范开发技术应用到安全策略模型的开发中,提出了开发安全策略形式规范的具体方法和步骤,并据此开发完成商务安全策略的Z形式规范。
第六:本文最后使用高级形式验证系统——Z/EVES对商务安全策略规范进行了形式分析和研究。在形式分析商务安全策略规范的基础上,对商务安全策
Security policy and security model act as the foundation for developing security-related products as well as building security systems. The commercial security policy based on the Clark-Wilson integrity model is a kind of constructing policy for security system applicable to commercial environment. Compared with the research depth and extension on military security policy characteristic of confidentiality, the research and application on commercial security policy characteristic of integrity still drops behind, which mainly results in the deficiency of understand to the application setting of commercial security policy as well as the policy itself. Therefore, it is essential to researches, in depth, investigate the commercial security policy.Research on the commercial security policy includes modeling of the security policy, formal analysis principle of security policy, the framework of commercial security policy and its formal analysis. In this thesis, the modeling and formal analysis of commercial security policy are studied, and the main results achieved are as follows:First, according to the different application settings of security policies, as far as we know, it is the first attempt to divide the security policies into two types: the developing policies for security product and the constructing policies for commercial security system. On the one side, the application scenario is considered the key to precisely understanding the security policy; On the other hand, it acts as an obstacle to model and generalize the commercial security policy.Second, all aspects of the security modeling are investigated, and an applied, easy operated security policy modeling technique with firm theoretical foundation is presented.Third, according to the fact that the essence of commercial security is to effectively control the applications in the system, a formal framework for commercial security policy is proposed, and for the first time the formal modeling of the Clark-Wilson integrity policy is completely made. The framework has the virtues of well-extension and high compatibility.Forth, a creative multi-policy security monitoring framework, aiming for supervising the behaviors in system, is proposed. This framework can solve the
problems such as redundancy of audit data and delay of detecting abnormalities which are existed in the traditional audit sub-systems.Fifth, aiming for solving inconsistence between the security policy model and the security function specification, the security functionality specification technique is directly applied to the development of the security policy model. In addition, the detailed methods and steps to establish security policy specification, based on which the Z formal specification for commercial security policy is built, is presented.Lastly, the high-level formal verification system-Z/EVES is adopted to analyze the commercial security policy specification. Based on the analysis of the commercial security policy specification, the commercial security policy specification is further adjusted and made more reasonable in terms of syntax and semantics. Furthermore, the formal proof about security properties shows that the commercial policy is consistent. It is the first time to analyze the rationality and validity of the Clark-Wilson integrity security policy formally and comprehensively.
商务安全策略研究的主要内容包括:安全策略制模和形式分析原理、商务安全策略框架模型研究以及形式分析。围绕着商务安全策略的制模和形式分析,本文取得了以下几个方面的成果:
第一:首次从安全策略应用场景的角度出发,把安全策略分为安全产品开发策略和安全系统构建策略,经研究发现策略应用场景是精确理解安全策略的一个关键因素,也是妨碍对以Clark-Wilson完整性安全策略为代表的商务安全策略进行制模和推广使用的主要原因之一。
第二:深入讨论了安全模型开发的方方面面,并且提出了一个实用的、易操作的、具有相当理论基础的安全策略制模方法。
第三:针对商务安全的本质就是对系统中的应用进行有效控制的指导思想,提出了一个商务安全策略的形式框架,首次完整地对Clark-Wilson完整性安全策略进行了形式制模,该框架具有扩展性好、兼容性高等方面的优势。
第四:提出了一个新颖的、可以依据系统所实现的策略进行安全监视的多策略安全监视框架。该框架可以很好地解决传统审计中的数据冗余过大和系统异常侦测时延过长的问题。
第五:针对当前形式开发中所存在的安全策略模型到安全功能规范之间的平滑过渡问题,本文直接把安全功能规范开发技术应用到安全策略模型的开发中,提出了开发安全策略形式规范的具体方法和步骤,并据此开发完成商务安全策略的Z形式规范。
第六:本文最后使用高级形式验证系统——Z/EVES对商务安全策略规范进行了形式分析和研究。在形式分析商务安全策略规范的基础上,对商务安全策
Security policy and security model act as the foundation for developing security-related products as well as building security systems. The commercial security policy based on the Clark-Wilson integrity model is a kind of constructing policy for security system applicable to commercial environment. Compared with the research depth and extension on military security policy characteristic of confidentiality, the research and application on commercial security policy characteristic of integrity still drops behind, which mainly results in the deficiency of understand to the application setting of commercial security policy as well as the policy itself. Therefore, it is essential to researches, in depth, investigate the commercial security policy.Research on the commercial security policy includes modeling of the security policy, formal analysis principle of security policy, the framework of commercial security policy and its formal analysis. In this thesis, the modeling and formal analysis of commercial security policy are studied, and the main results achieved are as follows:First, according to the different application settings of security policies, as far as we know, it is the first attempt to divide the security policies into two types: the developing policies for security product and the constructing policies for commercial security system. On the one side, the application scenario is considered the key to precisely understanding the security policy; On the other hand, it acts as an obstacle to model and generalize the commercial security policy.Second, all aspects of the security modeling are investigated, and an applied, easy operated security policy modeling technique with firm theoretical foundation is presented.Third, according to the fact that the essence of commercial security is to effectively control the applications in the system, a formal framework for commercial security policy is proposed, and for the first time the formal modeling of the Clark-Wilson integrity policy is completely made. The framework has the virtues of well-extension and high compatibility.Forth, a creative multi-policy security monitoring framework, aiming for supervising the behaviors in system, is proposed. This framework can solve the
problems such as redundancy of audit data and delay of detecting abnormalities which are existed in the traditional audit sub-systems.Fifth, aiming for solving inconsistence between the security policy model and the security function specification, the security functionality specification technique is directly applied to the development of the security policy model. In addition, the detailed methods and steps to establish security policy specification, based on which the Z formal specification for commercial security policy is built, is presented.Lastly, the high-level formal verification system-Z/EVES is adopted to analyze the commercial security policy specification. Based on the analysis of the commercial security policy specification, the commercial security policy specification is further adjusted and made more reasonable in terms of syntax and semantics. Furthermore, the formal proof about security properties shows that the commercial policy is consistent. It is the first time to analyze the rationality and validity of the Clark-Wilson integrity security policy formally and comprehensively.
引文
[ABAD93] M. Abadi, L. Lamport, Composing specifications, Transactions on Programming Languages and Systems, January 1993, pp. 73-132.
[ABRA95] M. Abrams, M. Joyce, Trusted System Concepts, Computers and Security, Vol.14 No.1, 1995,pp.45-56.
[ALKA02] M. Al-Kahtani, R. Sandhu, A Model for Attribute-Based User-Role Assignment, In: Proceedings of the 18' Annual Computer Security Applications Conference, Las Vegas, Nevada, USA, December 2002, pp.353-362.
[ANDE80] J. Anderson, Computer Security Threat Monitoring and Surveillance, Tech. Rep., James P Anderson Co., Fort Washington, PA, Apr. 1980.
[ANDR86] P. Andrews, An Introduction to Mathematical Logic and Type Theory: to Truth through Proof, Computer Science and Applied Mathematics, Academic Press, 1986.
[ATLU96] V. Atluri, W. K-Huang, An Authorization Model for Workflows, In: Proceedings of Computer Security ESORICS'96, Eds.: E.Bertino et al, Rome, September 1996, Springer-Verlag, pp.44-64.
[ALTU97] V. Atluri, S. Jajodia, T. Keefe, C. McCollum, R. Mukkamala, Multilevel secure transaction processing: Status and prospects, In: Database Security X: Status and Prospects, P. Samarati and R. Sandhu, eds., Chapman and Hall, London, 1997, pp. 79-98.
[ANDE72] J. Anderson, Computer Security Technology Planning Study, ESD-TR-73-51, Air Force Electronic Systems Division, Hanscom AFB, Bedford, MA, 1972. (Also available as Vol. I,DITCAD-758206. Vol. II, DITCAD-772806)
[ASPI00a] D. Aspinall, Proof General: A generic tool for proof development, 2000. http://www. dcs.ed.ac.uk/home/proofgen/.
[ASPI00b] D. Aspinall, Protocols for interactive e-proof Technical Report CSE 00- 009, Oregon Graduate Institute, 2000.
[BADG89] L. Badger, A Model for Specifying Multi-Granularity Integrity Polices, IEEE Symposium on Security and Privacy, Oakland, CA, 1989, pp.269-277.
[BARD94] R. Barden, S. Stepney, D. Cooper, Z In Practice, Prentice Hall, 1994.
[BARJ98] M. Barjaktarovic, The State-of-the-art in Formal Methods, AFOSR Summer Research technical report for Rome Research Site, AFRL/IFGB.
[BARK00a] E. Barka , R. Sandhu, A Role-Based Delegation Model and Some Extensions, In: Proceedings of the 23rd NIST-NCSC National Information Systems Security Conference, Baltimore, USA, Oct. 2000, pp. 101-114.
[BARK00b] E. Barka, R. Sandhu, Framework for Role-Based Delegation Models, In: Proceedings of the 16th IEEE Annual Computer Security Applications Conference, New Orleans, Louisiana, USA, Dec. 2000, pp. 168-175.
[BELL76] D. Bell, L. LaPadula, Secure computer system: Unified exposition and Multics interpretation, Mitre Technical Report MTR-2997, Mitre Corp., Bedford, MA, March 1976.
[BERG99] S. Berghofer, M.Wenzel, Inductive datatypes in HOL - lessons learned in Formal-Logic Engineering, In: Y. Bertot, G Dowek, A. Hirschowitz, C. Paulin, L. Thery, editors, Theorem Proving in Higher Order Logics: TPHOLs '99, volume 1690 of LNCS, 1999.
[BERN87] P. Bernstein, V. Hadzilacos, N. Goodman, Concurrency Control and Recovery in Database Systems, Addison-Wesley Publishing Company, 1987.
[BERT01] E. Bertine, B. Catania, E. Ferrari, A Nested Transaction Model for Multilevel Secure Database Management Systems, ACM Transaction on Information and System Security, Vol.4, No.4, November 2001, pp.321-370.
[BIBA77] K. Biba, Integrity Consideration for Secure Computer Systems, MITRE TR-3153, MITRE Corporation, Bedford, MA, April 1977.
[BIDD79] B. Biddle, E. Thomas, editors. Role Theory: Concepts and Research. Robert E. Krieger Publishing, New York, 1979.
[BISH02] M. Bishop, Computer Security: Art and Science, Addison-Wiley, New York, 2002.
[BISH89] M. Bishop, A Model of Security Monitoring, In: IEEE 5th Annual Computer Security Applications Conference, December 1989, Tucson Arizona, pp.46-52.
[BISH95] M. Bishop, A Standard Audit Trail Format, In: Proceedings of the Eighteenth National Information Systems Security Conference, Oct. 1995, pp. 136-145.
[BISH96] M. Bishop, C. Wee, J. Frank, Goal-Oriented Auditing and Logging, http://seclab.cs. ucdavis. edu/papers/tocs-96.pdf, 1996.
[BONY81] D. Bonyun, The Role of a Well-Defined Auditing Process in the Enforcement of Privacy Policy and Data Security, In: IEEE Symposium on Security and Privacy, Oakland CA., 1981, pp. 19-26.
[BOSW95] A. Boswell, Specification and Validation of a Security Policy Model, IEEE Transaction Software Engineering, 21(2), 1995, pp.63-68.
[CARL98] T. Carla, E. Brodley, Temporal Sequence Learning and Data Reduction for Anomaly Detection, In: Proceedings of the 5th Conference on Computer & Communications Security, New York, ACM Press, 1998, pp. 150-158.
[CESG95] Communications Electronics Security Group, CESG computer security manual "F": A formal development method for high assurance systems, Issue 1.1, Cheltenham, UK, July 1995.
[CHEH81] M. Cheheyl, M. Gasser, G. Huff, J. Millen, Verifying Security, ACM Computing Surveys, 13(3), September 1981, pp. 279-240.
[CHUR40] A. Church, A formulation of the simple theory of types, Journal of Symbolic Logic, 5, 1940, pp.5 6-68.
[CLAR87] D. Clark, D. Wilson, A Comparison of Commercial and Military Computer Security Policies, In: IEEE Symposium on Security and Privacy, Oakland, CA, 1987, pp. 184-194.
[COHE88] F. Cohen, Models of Practical Defenses Against Computer Viruses, IFIP-TC11, Computers and Security, Vol.7. No.6, 1988.
[DEFE97] (Part 1: Requirements, Part 2: Guidance). Defence Standard 00-55, Issue 2, Requirements for Safety Related Software in Defence Equipment, Ministry of Defence, Directorate of Standardisation Kentigern House, 65 Brown Street, Glasgow G2 8EX, UK., 1997.
[DENN90] D. Denning, T. Lunt, A Multilevel Relational Data Model, In: IEEE Symposium on Security and Privacy. New York: IEEE Computer Society Press, 1990. pp.220-234.
[DIVI90] B. Di Vito, P. Palmquist, E. Anderson, M. Johnston, Specification and Verification of the ASOS Kernel, In: IEEE Symposium on Security and Privacy, Oakland, CA, 1990, pp.60-74.
[EWIC98] European Workshop on Industrial Computer Systems, Technical Committee 7 (Safety, Reliability, Security), Formal Methods subgroup, Guidance on the Use of Formal Methods in the Development of High Integrity Industrial Computer Systems. Parts I, II, working paper 4001, June 1998.
[FERR01] D. Ferraiolo, R. Sandhu, S. Gavrila, D. Kuhn, R. Chandramouli, Proposed NIST Standard for Role-Based Access Control, ACM Transactions on Information and System Security (TISSEC),4(3), August 2001,pp.224-274.
[FERR92] D. Ferraiolo, D. Kuhn, Role-Based Access Control, In: 15th NCSC National Computer Security Conference, Baltimore, 1992.
[FERR95] D. Ferraiolo, J. Cugini, R. Kuhn, Role-Based Access Control (RBAC): Features and Motivations, In: Proceedings of the 11th Annual Computer Security Applications Conference, New Orleans, LA, USA, Dec. 1995, pp. 241-248.
[FOLE97] S. Foley, The Specification and Implement of 'Commercial' Security Requirments Including Dynamic Segregation of Duties, In: Proceedings of the 4th ACM Conference on Computer and Communications Security, April 1-4, 1997, Zurich, Switzerland, ACM, 1997, pp.125-134.
[FOLE98] S. Foley, Evaluating System Integrity, In: ACM New Security Paradigm Workshop, Ontario, September 1998, Chariollsville, VA, USA, pp.40-47.
[FRAS94] M. Fraser, K. Kumar, V. Vaishnavi, Strategies for Incorporating Formal Specifications in Software Development, Communications of the ACM, Vol.37, No. 10, October 1994, pp.74-86.
[GASS88] M. Gasser, Building A Security Computer System, New York: Van Nostrand Reinhold Company, 1988.
[GLAS89] J. Glasgow, G. MacEwen, Obligation as the basis of integrity specification, Computer Security Foundations Workshop, MITRE Corp., Franconia, N. H., 1989, pp.64-70.
[GLAS92] J. Glasgow, G. MacEwen, A Logic for Reasoning About Security, ACM Transactions on Computer Systems, Vol. 10, No 3, August 1992, pp.226-264.
[GOED65] K. Goedel, On formally undecidable propositions of the principia mathematica and related systems, In: M. Davis, editor, The Undecidable, Raven Press, Hewlett, N. Y., 1965, pp. 5-38.
[GOOD82] D. Good, A. Siebert, L. Smith, Message Flow Modulator Final Report, Technical Report ICSCACMP-34, Institute for Computing Science, University of Texas at Austin, December, 1982.
[GOOD84] D. Good, B. Divito, M. Smith, Using the Gypsy Methodology, Institute for Computing Science, University of Texas at Austin, June, 1984.
[GOOD86] D. Good, R. Akers, L. Smith, Report on Gypsy 2.05, Tech. Rept. ICSCA-CMP-48, Institute for Computer Science and Computing Applications, The University of Texas at Austin, February, 1986.
[GORD79] M. Gordon, Robin Milner, C. Wadsworth, Edinburgh LCF: a Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science, Springer-Verlag, 1979.
[GOVE91] R. Gove, L. Jaworski, J. Williams, To Bell and back: Developing a formal security policy model for a C2 system, In: Proceeding Seventh Annual Computer Security Applications Conference, IEEE, San Antonio, TX, December 1991.
[GRAU89] R. Graubert, On the Need for a Third Form of Access Control, Proceedings of the 12th National Computer Security Conference, Gaithersburg, MD, October 1989, pp.296-304.
[HAYE87] I. Hayes (editor), Specification Case Studies, Prentice-Hall, Englewood Cliffs, N.J.,1987.
[HITC00] M. Hitchens, V. Varadharajan, Design and Specification of Role Based Access Control Policies, In: Proceeding oflEE-Software, vol. 147, no. 4, Aug. 2000, pp. 117-129.
[HOPC01] J. Hopcroft, R. Motwani, J. Ullman, Introduction to Automata Theory, Languages, and Computation, 2th eds, Addison-Wesly, NY, 2001.
[IOS99] The International Organization for Standardization, Common Criteria for Information Technology Security Evaluation, ISO/IEC 15408: 1999(E), 1999.
[ITO86] K. Ito, (Ed.), Zermelo-Fraenkel Set Theory, §33B in: Encyclopedic Dictionary of Mathematics, 2nd ed., Vol. 1, Cambridge, MA: MIT Press, 1986, pp.146-148.
[JANS98] W. Jansen, A Revised Model for Role Based Access Control, National Institute of Standards and Technology (NIST), USA, NIST-IR 6192, July 1998.
[JENS74] K. Jensen, N. Wirth, Pascal User Manual and Report, Springer-Verlag, 1974.
[JIAN03] 蒋宗礼,姜守旭,形式化语言与自动机理论,清华出版社,北京,2003.
[JUEN88] R. Jueneman, Integrity Controls for Military and Commercial Application, In: Fourth Aerospace Computer Security Applications Conference, Orland, Florida, 1988, pp.298-322.
[KARG88] P. Karger, Implementing Commercial Data Integrity with Secure Capabilities, In: IEEE Symposium on Security and Privacy, Oakland, CA., 1988, pp. 130-139.
[KARG90] P. Karger, M. Zurko, D. Bonin, A. Mason, C. Kahn, A VMM Security Kernel for The Vax Architecture, IEEE Computer Society Symposium on Security and Privacy, Oakland, CA, 1990,pp.2-19.
[KATZ89] S. Katzke, Z. Ruthberg, editors, Report of the Invitational Workshop on Data Integrity. NIST, Special Publication 500-160, 1989.
[KEET82] J. Keeton-Williams, S. Ames, B. Hartman, R. Tyler, Verification of the ACCAT-Guard Downgrade Trusted Process, Tech. Rept. NTR-8463, The Mitre Corporation, Bedford, MA., 1982.
[KENN01] C. Kenneth, P. Jane, Management Information Systems: Organization and Technology in the Networked Enterprise, 6th ed., Prentice Hall, Pearson Education 2000, pp1-159.
[KERN02] A. Kern, Advanced Features for Enterprise-Wide Role-Based Access Control, In: Proceedings of the 18th Annual Computer Security Applications Conference, Las Vegas, USA, December 2002, pp.333-342.
[KERN03]A. Kern, A. Schaad, J. Moffett, An administration concept for the enterprise role-based access control model, In: Proceedings of the 8th ACM symposium on Access control models and technologies (SACMAT 2003), Como, Italy, June 02-03, 2003, pp.3-11.
[KOLY96] T. Kolyang, B. Santen, B. Wolff, A Structure Preserving Encoding of Z in Isabelle/ HOL, In: J. Wright, J. Grundy, J. Harrison (eds.), Theorem Proving in Higher Order Logics - 9th International Conference, Lecture in Notes in Computer Science 1125, Springer Verlag, 1996.
[KUMA95] S. Kumar, Classification and Detection of Computer Intrusions, PhD Dissertation, Purdue University, August 1995
[LAND81] C. Landwehr, Formal Models for Computer Security, ACM Computing Surveys, 13(3), 1981,pp.247-278.
[LAND84] C. Landwehr, C. Heitmeyer, J. McLean, A security model for military message systems, ACM Transactions on Computer Systems, 2(3), August 1984, pp. 198-222.
[LAPA95] L. LaPadula, Rule-Set Modeling of Truested Computer System, Essay 9 in: M. Abrams, S. Jajodia, H. Podell, Information Security-n Integrity Collection of Essays, IEEE Computer Society Press, 1995, pp. 187-226.
[LEE87] T. Lee, Using Mandatory Integrity to Enforce "Commercial" Security, In: IEEE Symposium on Security and Privacy, Oakland, CA. 1987, pp. 140-146.
[LEE98] W. Lee, S. Stolfo, Data mining approaches for intrusion detection, In: Proceedings of the 7th USENIX Security Symposium, San Antonio, Texas, U.S.A., 1998, pp.79-94.
[LEE99] E. Lee, Essays About Computer Security, University of Cambridge Computer Laboratory, 1999, pp. 141 -151.
[LETH00] T. Lethbridge, What Knowledge is Important to a Software Engineer, IEEE Computer, May 2000.
[LEVE90] N. Leveson, N. Guest Editor, Introduction: Formal Methods in Software Engineering, IEEE Transactions in Software Engineering, September 1990.
[LEVI79] K. Levitt, L. Robinson, B. Silverberg, The HDM handbook, vols. 1-3, Computer Science Lab., SRI International, Menlo Park, Cahf., June 1979.
[LIND69] R. Linde, C. Weissman, C. Fox, The Adept-50 Time-Sharing System, In: AFlPS Conference Proceedings, Fall Joint Computer Conference, Volume 35, 1969, pp.35-50.
[LIPN82] S. Lipner, Non-Discretionary Control for Commercial Applications, In: IEEE Symposium on Security and Privacy, Oakland, CA, 1982, pp.2-10.
[LUPU95] E. Lupu, D. Marriott, M. Sloman, N. Yialelis, A Policy Based Role Framework for Access Control, In: Proceedings of the 1st ACM/NIST Workshop on Role Based Access Control, National Institute of Standards and Technology, Gaithersburg, Maryland, USA, Dec. 1995, pp. Ⅱ15-Ⅱ24.
[LYNC86] N. lynch, M. Merritt, Introduction to The Theory of Nested Transactions, Massachusetts Institute of Technology, Cambridge, Mass., Report MIT/LCS/TR-367, 1986.
[MARS02] A. Marshall, A Financial Institution's Legacy Mainframe Access Control System in Light of the Proposed NIST RBAC Standard, In: Proceedings of the 18th Annual Computer Security Application Conference, Las Vegas, Nevada, USA, December 2002, pp.382-390.
[MAYF91] T. Mayfield, J. Roskos, S. Welke, J. Boone, Integrity in Automated Information Systems, Tech. Rep, 79-91, NCSC, 1991.
[MCLE85] J. McLean, A comment on the "Basic Security Theorem" of Bell and LaPadula, Information Processing Letters, 20(2), February 1985, pp. 67-70.
[MCLE88] J. McLean, The algebra of security, In: Proceedings 1988 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, April 1988.
[MCLE90] J. McLean, The Specification and Modeling of Computer Security, IEEE Computer, Vol.23, NO.l, 1990, pp.9-16.
[MCLE92] J. McLean, Proving noninterference and functional correctness using traces, Journal of Computer Security, 1(1), 1992.
[MCLE94] J. Mclean, Security Models, In: J. Marciniak, eds., Encyclopedia of Software Engineering, Wiley Press, 1994.
[MEAL55] G. Mealy, A Method for Synthesizing Sequential Circuits, Bell System Technical Journal, vol.34, no.5, Sept. 1955, pp. 1,045-1,079,
[MEIS97] I. Meisels, M. Saaltink, The Z/EVES Reference Manual (for Version 1.5), Technical Report, TR-97-5493-03d, ORA Canada, September 1997.
[MIA099] 缪淮扣,李刚,朱关铭,软件工程语言——Z,上海:上海科学技术文献出版社,1999.
[MICR04] Microsoft Corporation, Microsoft Encarta Reference Library 2005, Redmond, WA. 98052-6399, USA, 2004.
[MILL89] J. Millen, Models of multilevel computer security, Mitre Technical Report MTR-10537, The Mitre Corporation, January 1989. Also in: Advances in Computers, Vol. 28, Academic Press.
[MILL90] D. Miller, R. Baldwin, Access control by boolean expression evaluation, In: Fifth Annual Computer Security Applications Conference, Tucson, AZ, 1990, IEEE Comput. Soc. Press, pp. 131-139.
[MOSS81] J. Moss, Nested Transaction: An Approach to Reliable Distributed Computing, Massachusetts Institute of Technology, Cambridge, Mass., Report MIT/LCS/TR-260, 1981.
[MOYE01] M. Moyer, M. Ahamad, Generalized Role-Based Access Control, In: Proceedings of the 21st IEEE International Conference on Distributed Computing Systems, Meza, Arizona, USA, Apr. 2001, pp. 391-398.
[MULL99] O. Muller, T. Nipkow, D. Oheimb, O. Slotosch, HOLCF = HOL + LCF, Journal of Functional Programming, 9, 1999.
[NCSC85] National Computer Security Center, DoD 5200.28-STD, Trusted Computer Systems Evaluation Criteria, Ft. Meade, MD, December 1985.
[NCSC88] National Computer Security Center, A Guide to Understanding Audit in Trusted Systems, Version 2, NCSC-TG-001, Fort George G. Meade, MD, 1988.
[NCSC92] National Computer Security Center, A guide to understanding security modeling in trusted systems, Technical Report NCSC-TG-10, National Security Agency, October 1992.
[NELS79]G. Nelson, D. Oppen, Simplification by cooperating decision procedures, ACM Transactions on Programming Languages and Systems, 1(2), 1979, pp.243-257.
[NIPK01a] T. Nipkow, L. Paulson, Isabelle/HOL - The Tutorial, 2001, Part of the Isabelle99-2 distribution, http://isabelle.in.tum.de/doc/rutorial.pdf.
[NIPKOlb] T. Nipkow, L. Paulson, M. Wenzel, Isabelle's Logics: HOL, 2001, Part of the Isabelle99-2 distribution, http://isabelle.in.tum.de/doc/logics-HOL.pdf.
[NYAN94] M. Nyanchama, Commercial Integrity, Roles and Object Orientation, PhD thesis, Department of Computer Science, Faculty of Graduate Studies, University of Western Ontario, London, Ontario, Canada, 1994.
[OH02] S. Oh, R. Sandhu, A Model for Role Administration Using Organization Structure, In: Proceedings of the 7th ACM Symposium on Access Control Models and Technologies (SACMAT 2002), Monterey, California, USA, June 2002, pp. 155-168.
[OHEI01] D. Oheimb, Analyzing Java in Isabelle/HOL - Formalization, Type Safety and Hoare Logic, PhD thesis, TU M unchen, 2001.
[OTT01] A. Ott, Rule Set Based Access Control in Linux, RSBAC Home Page, http://www.rsbac. org/.
[OZSU89] M. Ozsu, P. Valduriez, Principle of Distributed Database Systems, 2th ed., New Jersey: Prentice Hall, 1989, pp.25-51.
[PARN72] D. Parnas, A Technique for Software Module Specification with Examples, Communications of the ACM, Vol.15, No.5, May 1972, pp.330-336.
[PAUL86] L. Paulson, Natural deduction as higher-order resolution, Journal of Logic Programming, 3, 1986.
[PAUL87] L. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge University Press, 1987.
[PAUL89] L. Paulson, The foundation of a generic theorem prover, Journal of Automated Reasoning, 5(3), 1989, pp. 363-397.
[PAUL90] L. Paulson, Isabelle: the next 700 theorem provers, In: P. Odifreddi, editor, Logic and Computer Science, Academic Press, 1990.
[PAUL93] L. Paulson, Set theory for verication: I. From foundations to functions, Journal of Automated Reasoning, 11(3), 1993.
[PAUL94a] L. Paulson, A fixed point approach to implementing (co)inductive definitions, In: A. Bundy, editor, 12th International Conference on Automated Deduction - CADE-12, volume 814 of LNAI, Springer, 1994, pp. 148-161.
[PAUL94b] L. Paulson, T. Nipkow, Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer, 1994.
[PAUL95] L. Paulson, Set theory for verication: II. Induction and recursion, Journal of Automated Reasoning, 15(2), 1995.
[PAUL97] L. Paulson, Generic automatic proof tools, In: R. Vero, editor, Automated Reasoning and its Applications: Essays in Honor of Larry Wos, MIT Press, 1997.
[PAUL99] L. Paulson, A generic tableau prover and its integration with Isabelle, Journal of Universal Computer Science, 5(3), 1999.
[PAYN93] C. Payne, J. Froscher, C. Landwehr, Toward a comprehensive INFOSEC certification methodology, In: Proceedings of the 16th National Computer Security Conference, NIST/NSA, Baltimore, MD, September 1993, pp. 165-172.
[PAYN95] C. Payne, Secure Policy Model, Navy Handbook for the Computer Security Certification of Trusted Systems, Chapter 3, NRL Technical Memorandum NRL/TM/5540:080A. Naval Research Laboratory, Washington, DC. January 1995.
[PCCI97] President's Commission on Critical Infrastructure, Critical Foundations: Protecting America's Infrastructures, October 1997.
[PERI94] R. Peri, Specification and Verification of Security Policies, PhD thesis, the Faculty of the School of Engineering and Applied Science, University of Virginia, Charlottesville, VA, USA, 1994
[PICC87] J. Picciotto, The Design of An Effection Auditing Subsystem, In: IEEE Symposium on Security and Privacy, Oakland CA., 1987, pp.13-22.
[POVE99] D. Povey, Optimistic Security: A New Access Control Paradigm, In: ACM New Security Paradigm Workshop, Ontario, September 1999, Canada, pp.40-45.
[PRIC73] W. Price, Implications of a Virtual Memory Mechanism for Implementing Protection in a Family of Operating Systems, PhD thesis, Carnegie-Mellon University, June 1973.
[RAMA00] R. Ramakrishnan, J. Gehrke, Database Management Systems (2th ed.), McGraw-Hill, 2000, pp.51-83.
[REGE95] F. Regensburger, HOLCF: Higher order logic of computable functions, In: E. Schubert, P. Windley, J. Alves-Foss, editors, Higher Order Logic Theorem Proving and its Applications, volume 971 of LNCS, 1995.
[SAAL97] M. Saaltink. Domain checking Z specifications. In: C. Holloway, K. Hayhurst, editors, LFM' 97: Fourth NASA Langley Formal Methods Workshop, Hampton, VA, September 1997, pp. 185-192.
[SAMA00] P. Samarati, S. Vimercati, Access Control: Policies, Models, and Mechanisms, Revised versions of lectures given during the IFIP WG 1.7 International School on Foundations of Security Analysis and Design: Tutorial Lectures, September 01, 2000, pp.137-196.
[SAND88] R. Sandhu, Transaction Control Expressions for Separation of Duties, In: Fourth Aerospace Computer Security Applications Conference, Orland, Florida, 1988, pp.298-322.
[SAND95] R. Sandhu, Roles Versus Groups, In: Proceedings of the First ACM Workshop on Role-Based Access Control, Gaithersburg, Maryland, USA, December 1995, pp. 125-126.
[SAND96] R. Sandhu, E. Coyne, H. Feinstein, C. Youman, Role-Based Access Control Models, IEEE Computer, 29(2), February 1996, pp.38-47.
[SAND97] R. Sandhu, V. Bhamidipati, The ARBAC97 model for Role-based administration of Roles: Preliminary Description and Outline, In: Proceedings of second ACM Workshop on Role-Based Access Control, November 1997.
[SAND99a] R. Sandhu, V. Bhamidipati, Role-Based Administration of User-Role Assignment: The URA97 Model and its Oracle Implementation, Journal of Network and Computer Applications, 22(3), July 1999.
[SAND99b] R. Sandhu, Q. Munawer, The ARBAC99 Model for Administration of Roles, In: Proceedings of the 18' Annual Computer Security Applications Conference, Phoenix, Arizona, USA, December 1999, pp.229-238.
[SAYD89] O. Saydjari, J. Beckman, J. Leaman, LOCK trek: Navigating uncharted space, In: IEEE Symposium on Research in Security and Privacy, Oakland, CA, 1989, pp. 167-175.
[SCHA01] A. Schaad, J. Moffett, J. Jacob, The Role-Based Access Control System of a European Bank: A Case Study and Discussion, In: Proceedings of the 6th ACM Symposium on Access Control Models and Technologies, Litton-TASC, Chantilly, Virginia, USA, May 2001, pp. 3-9.
[SCHN99] F. Schneider (Ed.), Trust in Cyberspace, Committee on Information Systems trustworthiness, National Research Council, 1999.
[SEID90] K. Seiden, J. Melanson, The Auditing Facility for a VMM Security Kernel, In: IEEE Symposium on Security and Privacy, Oakland CA, May 1990, pp.2-19.
[SHAM79] A. Shamir, How to Share a Secret, Communications of the ACM, 22(11), November 1979, pp. 612-613
[SIHA01] 卿斯汉,刘文清,刘海峰,操作系统安全导论,北京:科学出版社,2001年1月.
[SIHA04a] 卿斯汉,刘文清,温红子,刘海峰,操作系统安全,北京:清华出版社,2004年7月.
[SIHA04b] 卿斯汉,温红子,雷浩,王建,基于Clark-Wilson完整性策略的安全监视模型,软件学报,Vol.15 NO.8,2004,pp.1124-1132.
[SIMO01] E Simone, IT-Security and Privacy, Berlin: Springer-Verlag, 2001.
[SLIN96] K. Slind, Function definition in higher order logic, In: J. Wright, J. Grundy, J. Harrison, editors, Theorem Proving in Higher Order Logics: TPHOLs '96, volume 1125 of LNCS, 1996.
[SLIN97] K. Slind, Derivation and use of induction schemes in higher-order logic, In: E. Gunter, A. Felty, editors, Theorem Proving in Higher Order Logics: TPHOLs '97, volume 1275 of LNCS, 1997.
[SMIT81] M. Smith, A. Siebert, B. Divito, D. Good, A Verified Encrypted Packet Interface, ACM Software Engineering Notes 6, 3, July 1981.
[SMIT88] B. Smith, C. Reese, K. Lindsay, B. Crane, A Description of a Formal Verification and Validation (FVV) Process, In: Proceedings of the 1988 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, August 1988, pp.401-408.
[SPIV93] J. Spivey, The fuzz Manual, Second edition, J. Spivey Computing Science Consultancy, May 1993.
[STER91] D. Sterne, On the buzzword "security policy", In: Proceedings Symposium on Research in Security and Privacy, IEEE, June 1991.
[THOM94] R. Thomas, R. Sandhu, Conceptual Foundations for a model of Task-Based Authorizations, In: Proceedings 7th Computer Security Foundations Workshop, IEEE CS Press, Los Alamitos, CA, June 1994, pp.66-79
[THOM97] R. Thomas, R. Sandhu, Task-Based Authorization Controls (TBAC): A Family of Models for Active and Enterprise-Oriented Autorization Management, In: Proceedings of the IFIP TC11 WG11.3 Eleventh International Conference on Database Seeurty Ⅺ: Status and Prospects, August 10-13, 1997, pp. 166-181.
[TOMA92] O. Tomas, A Structured Approach to Computer Security, Department of Computer Engineering, Chalmers University of Technology, Gothenburg, Technical Report No. 122, 1992.
[VIEN93] R. Vienneau, A Review of Formal Methods, Kaman Sciences Corporation, 1993.
[WEIS69] C. Weissman, Security Controls In The Adept-50 Time Sharing System, In: AFIPS Conference Proceedings, Fall Joint Computer Conference, Volume 35, 1969, pp. 119-133.
[WEIS70] C. Weissman, Trade-Off Considerations in Security System Design, SDC-SP 3548, September 10, 1970, also Data Management April 1972.
[WETS99] WetStone Technologies, Inc., Formal Methods Framework, final month status report, Contract # F30602-99-C-0166, October 26, 1999, available http://www.cs.utexas.edu/~csed/ FM/docs/FMFramework.pdf.
[WIED01] F. Wiedijk, Digital math WWW page, 2001. http://www.cs.kun.nl/~freek/ digimath/.
[WING90] J. Wing, A Specifier's Introduction to Formal Methods, IEEE Computer, Vol.23, No.9, September 1990, pp.8-23.
[WISE91] S. Wiseman, The Conflict between Confidentiality and Integrity, In: Proceedings 4th Workshop on the Foundations of Computer Security, IEEE Computer Society Press 1991, pp. 241-242.
[WOOD96] J. Woodcock, J. Davies, Using Z, Prentice Hall, 1996.
[ZEIG76] B. Zeigler, Theory of Modelling and Simulation, Wiley, New York, NY, 1976.
[ZHAN01] L. Zhang, G. Ahn, B. Chu, A Rule-Based Framework for Role-Based Delegation, In: Proceedings, of the 6th ACM Symposium on Access Control Models and Technologies, Litton-TASC, Chantilly, Virginia, USA, May 2001, pp. 153-162.
[ABRA95] M. Abrams, M. Joyce, Trusted System Concepts, Computers and Security, Vol.14 No.1, 1995,pp.45-56.
[ALKA02] M. Al-Kahtani, R. Sandhu, A Model for Attribute-Based User-Role Assignment, In: Proceedings of the 18' Annual Computer Security Applications Conference, Las Vegas, Nevada, USA, December 2002, pp.353-362.
[ANDE80] J. Anderson, Computer Security Threat Monitoring and Surveillance, Tech. Rep., James P Anderson Co., Fort Washington, PA, Apr. 1980.
[ANDR86] P. Andrews, An Introduction to Mathematical Logic and Type Theory: to Truth through Proof, Computer Science and Applied Mathematics, Academic Press, 1986.
[ATLU96] V. Atluri, W. K-Huang, An Authorization Model for Workflows, In: Proceedings of Computer Security ESORICS'96, Eds.: E.Bertino et al, Rome, September 1996, Springer-Verlag, pp.44-64.
[ALTU97] V. Atluri, S. Jajodia, T. Keefe, C. McCollum, R. Mukkamala, Multilevel secure transaction processing: Status and prospects, In: Database Security X: Status and Prospects, P. Samarati and R. Sandhu, eds., Chapman and Hall, London, 1997, pp. 79-98.
[ANDE72] J. Anderson, Computer Security Technology Planning Study, ESD-TR-73-51, Air Force Electronic Systems Division, Hanscom AFB, Bedford, MA, 1972. (Also available as Vol. I,DITCAD-758206. Vol. II, DITCAD-772806)
[ASPI00a] D. Aspinall, Proof General: A generic tool for proof development, 2000. http://www. dcs.ed.ac.uk/home/proofgen/.
[ASPI00b] D. Aspinall, Protocols for interactive e-proof Technical Report CSE 00- 009, Oregon Graduate Institute, 2000.
[BADG89] L. Badger, A Model for Specifying Multi-Granularity Integrity Polices, IEEE Symposium on Security and Privacy, Oakland, CA, 1989, pp.269-277.
[BARD94] R. Barden, S. Stepney, D. Cooper, Z In Practice, Prentice Hall, 1994.
[BARJ98] M. Barjaktarovic, The State-of-the-art in Formal Methods, AFOSR Summer Research technical report for Rome Research Site, AFRL/IFGB.
[BARK00a] E. Barka , R. Sandhu, A Role-Based Delegation Model and Some Extensions, In: Proceedings of the 23rd NIST-NCSC National Information Systems Security Conference, Baltimore, USA, Oct. 2000, pp. 101-114.
[BARK00b] E. Barka, R. Sandhu, Framework for Role-Based Delegation Models, In: Proceedings of the 16th IEEE Annual Computer Security Applications Conference, New Orleans, Louisiana, USA, Dec. 2000, pp. 168-175.
[BELL76] D. Bell, L. LaPadula, Secure computer system: Unified exposition and Multics interpretation, Mitre Technical Report MTR-2997, Mitre Corp., Bedford, MA, March 1976.
[BERG99] S. Berghofer, M.Wenzel, Inductive datatypes in HOL - lessons learned in Formal-Logic Engineering, In: Y. Bertot, G Dowek, A. Hirschowitz, C. Paulin, L. Thery, editors, Theorem Proving in Higher Order Logics: TPHOLs '99, volume 1690 of LNCS, 1999.
[BERN87] P. Bernstein, V. Hadzilacos, N. Goodman, Concurrency Control and Recovery in Database Systems, Addison-Wesley Publishing Company, 1987.
[BERT01] E. Bertine, B. Catania, E. Ferrari, A Nested Transaction Model for Multilevel Secure Database Management Systems, ACM Transaction on Information and System Security, Vol.4, No.4, November 2001, pp.321-370.
[BIBA77] K. Biba, Integrity Consideration for Secure Computer Systems, MITRE TR-3153, MITRE Corporation, Bedford, MA, April 1977.
[BIDD79] B. Biddle, E. Thomas, editors. Role Theory: Concepts and Research. Robert E. Krieger Publishing, New York, 1979.
[BISH02] M. Bishop, Computer Security: Art and Science, Addison-Wiley, New York, 2002.
[BISH89] M. Bishop, A Model of Security Monitoring, In: IEEE 5th Annual Computer Security Applications Conference, December 1989, Tucson Arizona, pp.46-52.
[BISH95] M. Bishop, A Standard Audit Trail Format, In: Proceedings of the Eighteenth National Information Systems Security Conference, Oct. 1995, pp. 136-145.
[BISH96] M. Bishop, C. Wee, J. Frank, Goal-Oriented Auditing and Logging, http://seclab.cs. ucdavis. edu/papers/tocs-96.pdf, 1996.
[BONY81] D. Bonyun, The Role of a Well-Defined Auditing Process in the Enforcement of Privacy Policy and Data Security, In: IEEE Symposium on Security and Privacy, Oakland CA., 1981, pp. 19-26.
[BOSW95] A. Boswell, Specification and Validation of a Security Policy Model, IEEE Transaction Software Engineering, 21(2), 1995, pp.63-68.
[CARL98] T. Carla, E. Brodley, Temporal Sequence Learning and Data Reduction for Anomaly Detection, In: Proceedings of the 5th Conference on Computer & Communications Security, New York, ACM Press, 1998, pp. 150-158.
[CESG95] Communications Electronics Security Group, CESG computer security manual "F": A formal development method for high assurance systems, Issue 1.1, Cheltenham, UK, July 1995.
[CHEH81] M. Cheheyl, M. Gasser, G. Huff, J. Millen, Verifying Security, ACM Computing Surveys, 13(3), September 1981, pp. 279-240.
[CHUR40] A. Church, A formulation of the simple theory of types, Journal of Symbolic Logic, 5, 1940, pp.5 6-68.
[CLAR87] D. Clark, D. Wilson, A Comparison of Commercial and Military Computer Security Policies, In: IEEE Symposium on Security and Privacy, Oakland, CA, 1987, pp. 184-194.
[COHE88] F. Cohen, Models of Practical Defenses Against Computer Viruses, IFIP-TC11, Computers and Security, Vol.7. No.6, 1988.
[DEFE97] (Part 1: Requirements, Part 2: Guidance). Defence Standard 00-55, Issue 2, Requirements for Safety Related Software in Defence Equipment, Ministry of Defence, Directorate of Standardisation Kentigern House, 65 Brown Street, Glasgow G2 8EX, UK., 1997.
[DENN90] D. Denning, T. Lunt, A Multilevel Relational Data Model, In: IEEE Symposium on Security and Privacy. New York: IEEE Computer Society Press, 1990. pp.220-234.
[DIVI90] B. Di Vito, P. Palmquist, E. Anderson, M. Johnston, Specification and Verification of the ASOS Kernel, In: IEEE Symposium on Security and Privacy, Oakland, CA, 1990, pp.60-74.
[EWIC98] European Workshop on Industrial Computer Systems, Technical Committee 7 (Safety, Reliability, Security), Formal Methods subgroup, Guidance on the Use of Formal Methods in the Development of High Integrity Industrial Computer Systems. Parts I, II, working paper 4001, June 1998.
[FERR01] D. Ferraiolo, R. Sandhu, S. Gavrila, D. Kuhn, R. Chandramouli, Proposed NIST Standard for Role-Based Access Control, ACM Transactions on Information and System Security (TISSEC),4(3), August 2001,pp.224-274.
[FERR92] D. Ferraiolo, D. Kuhn, Role-Based Access Control, In: 15th NCSC National Computer Security Conference, Baltimore, 1992.
[FERR95] D. Ferraiolo, J. Cugini, R. Kuhn, Role-Based Access Control (RBAC): Features and Motivations, In: Proceedings of the 11th Annual Computer Security Applications Conference, New Orleans, LA, USA, Dec. 1995, pp. 241-248.
[FOLE97] S. Foley, The Specification and Implement of 'Commercial' Security Requirments Including Dynamic Segregation of Duties, In: Proceedings of the 4th ACM Conference on Computer and Communications Security, April 1-4, 1997, Zurich, Switzerland, ACM, 1997, pp.125-134.
[FOLE98] S. Foley, Evaluating System Integrity, In: ACM New Security Paradigm Workshop, Ontario, September 1998, Chariollsville, VA, USA, pp.40-47.
[FRAS94] M. Fraser, K. Kumar, V. Vaishnavi, Strategies for Incorporating Formal Specifications in Software Development, Communications of the ACM, Vol.37, No. 10, October 1994, pp.74-86.
[GASS88] M. Gasser, Building A Security Computer System, New York: Van Nostrand Reinhold Company, 1988.
[GLAS89] J. Glasgow, G. MacEwen, Obligation as the basis of integrity specification, Computer Security Foundations Workshop, MITRE Corp., Franconia, N. H., 1989, pp.64-70.
[GLAS92] J. Glasgow, G. MacEwen, A Logic for Reasoning About Security, ACM Transactions on Computer Systems, Vol. 10, No 3, August 1992, pp.226-264.
[GOED65] K. Goedel, On formally undecidable propositions of the principia mathematica and related systems, In: M. Davis, editor, The Undecidable, Raven Press, Hewlett, N. Y., 1965, pp. 5-38.
[GOOD82] D. Good, A. Siebert, L. Smith, Message Flow Modulator Final Report, Technical Report ICSCACMP-34, Institute for Computing Science, University of Texas at Austin, December, 1982.
[GOOD84] D. Good, B. Divito, M. Smith, Using the Gypsy Methodology, Institute for Computing Science, University of Texas at Austin, June, 1984.
[GOOD86] D. Good, R. Akers, L. Smith, Report on Gypsy 2.05, Tech. Rept. ICSCA-CMP-48, Institute for Computer Science and Computing Applications, The University of Texas at Austin, February, 1986.
[GORD79] M. Gordon, Robin Milner, C. Wadsworth, Edinburgh LCF: a Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science, Springer-Verlag, 1979.
[GOVE91] R. Gove, L. Jaworski, J. Williams, To Bell and back: Developing a formal security policy model for a C2 system, In: Proceeding Seventh Annual Computer Security Applications Conference, IEEE, San Antonio, TX, December 1991.
[GRAU89] R. Graubert, On the Need for a Third Form of Access Control, Proceedings of the 12th National Computer Security Conference, Gaithersburg, MD, October 1989, pp.296-304.
[HAYE87] I. Hayes (editor), Specification Case Studies, Prentice-Hall, Englewood Cliffs, N.J.,1987.
[HITC00] M. Hitchens, V. Varadharajan, Design and Specification of Role Based Access Control Policies, In: Proceeding oflEE-Software, vol. 147, no. 4, Aug. 2000, pp. 117-129.
[HOPC01] J. Hopcroft, R. Motwani, J. Ullman, Introduction to Automata Theory, Languages, and Computation, 2th eds, Addison-Wesly, NY, 2001.
[IOS99] The International Organization for Standardization, Common Criteria for Information Technology Security Evaluation, ISO/IEC 15408: 1999(E), 1999.
[ITO86] K. Ito, (Ed.), Zermelo-Fraenkel Set Theory, §33B in: Encyclopedic Dictionary of Mathematics, 2nd ed., Vol. 1, Cambridge, MA: MIT Press, 1986, pp.146-148.
[JANS98] W. Jansen, A Revised Model for Role Based Access Control, National Institute of Standards and Technology (NIST), USA, NIST-IR 6192, July 1998.
[JENS74] K. Jensen, N. Wirth, Pascal User Manual and Report, Springer-Verlag, 1974.
[JIAN03] 蒋宗礼,姜守旭,形式化语言与自动机理论,清华出版社,北京,2003.
[JUEN88] R. Jueneman, Integrity Controls for Military and Commercial Application, In: Fourth Aerospace Computer Security Applications Conference, Orland, Florida, 1988, pp.298-322.
[KARG88] P. Karger, Implementing Commercial Data Integrity with Secure Capabilities, In: IEEE Symposium on Security and Privacy, Oakland, CA., 1988, pp. 130-139.
[KARG90] P. Karger, M. Zurko, D. Bonin, A. Mason, C. Kahn, A VMM Security Kernel for The Vax Architecture, IEEE Computer Society Symposium on Security and Privacy, Oakland, CA, 1990,pp.2-19.
[KATZ89] S. Katzke, Z. Ruthberg, editors, Report of the Invitational Workshop on Data Integrity. NIST, Special Publication 500-160, 1989.
[KEET82] J. Keeton-Williams, S. Ames, B. Hartman, R. Tyler, Verification of the ACCAT-Guard Downgrade Trusted Process, Tech. Rept. NTR-8463, The Mitre Corporation, Bedford, MA., 1982.
[KENN01] C. Kenneth, P. Jane, Management Information Systems: Organization and Technology in the Networked Enterprise, 6th ed., Prentice Hall, Pearson Education 2000, pp1-159.
[KERN02] A. Kern, Advanced Features for Enterprise-Wide Role-Based Access Control, In: Proceedings of the 18th Annual Computer Security Applications Conference, Las Vegas, USA, December 2002, pp.333-342.
[KERN03]A. Kern, A. Schaad, J. Moffett, An administration concept for the enterprise role-based access control model, In: Proceedings of the 8th ACM symposium on Access control models and technologies (SACMAT 2003), Como, Italy, June 02-03, 2003, pp.3-11.
[KOLY96] T. Kolyang, B. Santen, B. Wolff, A Structure Preserving Encoding of Z in Isabelle/ HOL, In: J. Wright, J. Grundy, J. Harrison (eds.), Theorem Proving in Higher Order Logics - 9th International Conference, Lecture in Notes in Computer Science 1125, Springer Verlag, 1996.
[KUMA95] S. Kumar, Classification and Detection of Computer Intrusions, PhD Dissertation, Purdue University, August 1995
[LAND81] C. Landwehr, Formal Models for Computer Security, ACM Computing Surveys, 13(3), 1981,pp.247-278.
[LAND84] C. Landwehr, C. Heitmeyer, J. McLean, A security model for military message systems, ACM Transactions on Computer Systems, 2(3), August 1984, pp. 198-222.
[LAPA95] L. LaPadula, Rule-Set Modeling of Truested Computer System, Essay 9 in: M. Abrams, S. Jajodia, H. Podell, Information Security-n Integrity Collection of Essays, IEEE Computer Society Press, 1995, pp. 187-226.
[LEE87] T. Lee, Using Mandatory Integrity to Enforce "Commercial" Security, In: IEEE Symposium on Security and Privacy, Oakland, CA. 1987, pp. 140-146.
[LEE98] W. Lee, S. Stolfo, Data mining approaches for intrusion detection, In: Proceedings of the 7th USENIX Security Symposium, San Antonio, Texas, U.S.A., 1998, pp.79-94.
[LEE99] E. Lee, Essays About Computer Security, University of Cambridge Computer Laboratory, 1999, pp. 141 -151.
[LETH00] T. Lethbridge, What Knowledge is Important to a Software Engineer, IEEE Computer, May 2000.
[LEVE90] N. Leveson, N. Guest Editor, Introduction: Formal Methods in Software Engineering, IEEE Transactions in Software Engineering, September 1990.
[LEVI79] K. Levitt, L. Robinson, B. Silverberg, The HDM handbook, vols. 1-3, Computer Science Lab., SRI International, Menlo Park, Cahf., June 1979.
[LIND69] R. Linde, C. Weissman, C. Fox, The Adept-50 Time-Sharing System, In: AFlPS Conference Proceedings, Fall Joint Computer Conference, Volume 35, 1969, pp.35-50.
[LIPN82] S. Lipner, Non-Discretionary Control for Commercial Applications, In: IEEE Symposium on Security and Privacy, Oakland, CA, 1982, pp.2-10.
[LUPU95] E. Lupu, D. Marriott, M. Sloman, N. Yialelis, A Policy Based Role Framework for Access Control, In: Proceedings of the 1st ACM/NIST Workshop on Role Based Access Control, National Institute of Standards and Technology, Gaithersburg, Maryland, USA, Dec. 1995, pp. Ⅱ15-Ⅱ24.
[LYNC86] N. lynch, M. Merritt, Introduction to The Theory of Nested Transactions, Massachusetts Institute of Technology, Cambridge, Mass., Report MIT/LCS/TR-367, 1986.
[MARS02] A. Marshall, A Financial Institution's Legacy Mainframe Access Control System in Light of the Proposed NIST RBAC Standard, In: Proceedings of the 18th Annual Computer Security Application Conference, Las Vegas, Nevada, USA, December 2002, pp.382-390.
[MAYF91] T. Mayfield, J. Roskos, S. Welke, J. Boone, Integrity in Automated Information Systems, Tech. Rep, 79-91, NCSC, 1991.
[MCLE85] J. McLean, A comment on the "Basic Security Theorem" of Bell and LaPadula, Information Processing Letters, 20(2), February 1985, pp. 67-70.
[MCLE88] J. McLean, The algebra of security, In: Proceedings 1988 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, April 1988.
[MCLE90] J. McLean, The Specification and Modeling of Computer Security, IEEE Computer, Vol.23, NO.l, 1990, pp.9-16.
[MCLE92] J. McLean, Proving noninterference and functional correctness using traces, Journal of Computer Security, 1(1), 1992.
[MCLE94] J. Mclean, Security Models, In: J. Marciniak, eds., Encyclopedia of Software Engineering, Wiley Press, 1994.
[MEAL55] G. Mealy, A Method for Synthesizing Sequential Circuits, Bell System Technical Journal, vol.34, no.5, Sept. 1955, pp. 1,045-1,079,
[MEIS97] I. Meisels, M. Saaltink, The Z/EVES Reference Manual (for Version 1.5), Technical Report, TR-97-5493-03d, ORA Canada, September 1997.
[MIA099] 缪淮扣,李刚,朱关铭,软件工程语言——Z,上海:上海科学技术文献出版社,1999.
[MICR04] Microsoft Corporation, Microsoft Encarta Reference Library 2005, Redmond, WA. 98052-6399, USA, 2004.
[MILL89] J. Millen, Models of multilevel computer security, Mitre Technical Report MTR-10537, The Mitre Corporation, January 1989. Also in: Advances in Computers, Vol. 28, Academic Press.
[MILL90] D. Miller, R. Baldwin, Access control by boolean expression evaluation, In: Fifth Annual Computer Security Applications Conference, Tucson, AZ, 1990, IEEE Comput. Soc. Press, pp. 131-139.
[MOSS81] J. Moss, Nested Transaction: An Approach to Reliable Distributed Computing, Massachusetts Institute of Technology, Cambridge, Mass., Report MIT/LCS/TR-260, 1981.
[MOYE01] M. Moyer, M. Ahamad, Generalized Role-Based Access Control, In: Proceedings of the 21st IEEE International Conference on Distributed Computing Systems, Meza, Arizona, USA, Apr. 2001, pp. 391-398.
[MULL99] O. Muller, T. Nipkow, D. Oheimb, O. Slotosch, HOLCF = HOL + LCF, Journal of Functional Programming, 9, 1999.
[NCSC85] National Computer Security Center, DoD 5200.28-STD, Trusted Computer Systems Evaluation Criteria, Ft. Meade, MD, December 1985.
[NCSC88] National Computer Security Center, A Guide to Understanding Audit in Trusted Systems, Version 2, NCSC-TG-001, Fort George G. Meade, MD, 1988.
[NCSC92] National Computer Security Center, A guide to understanding security modeling in trusted systems, Technical Report NCSC-TG-10, National Security Agency, October 1992.
[NELS79]G. Nelson, D. Oppen, Simplification by cooperating decision procedures, ACM Transactions on Programming Languages and Systems, 1(2), 1979, pp.243-257.
[NIPK01a] T. Nipkow, L. Paulson, Isabelle/HOL - The Tutorial, 2001, Part of the Isabelle99-2 distribution, http://isabelle.in.tum.de/doc/rutorial.pdf.
[NIPKOlb] T. Nipkow, L. Paulson, M. Wenzel, Isabelle's Logics: HOL, 2001, Part of the Isabelle99-2 distribution, http://isabelle.in.tum.de/doc/logics-HOL.pdf.
[NYAN94] M. Nyanchama, Commercial Integrity, Roles and Object Orientation, PhD thesis, Department of Computer Science, Faculty of Graduate Studies, University of Western Ontario, London, Ontario, Canada, 1994.
[OH02] S. Oh, R. Sandhu, A Model for Role Administration Using Organization Structure, In: Proceedings of the 7th ACM Symposium on Access Control Models and Technologies (SACMAT 2002), Monterey, California, USA, June 2002, pp. 155-168.
[OHEI01] D. Oheimb, Analyzing Java in Isabelle/HOL - Formalization, Type Safety and Hoare Logic, PhD thesis, TU M unchen, 2001.
[OTT01] A. Ott, Rule Set Based Access Control in Linux, RSBAC Home Page, http://www.rsbac. org/.
[OZSU89] M. Ozsu, P. Valduriez, Principle of Distributed Database Systems, 2th ed., New Jersey: Prentice Hall, 1989, pp.25-51.
[PARN72] D. Parnas, A Technique for Software Module Specification with Examples, Communications of the ACM, Vol.15, No.5, May 1972, pp.330-336.
[PAUL86] L. Paulson, Natural deduction as higher-order resolution, Journal of Logic Programming, 3, 1986.
[PAUL87] L. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge University Press, 1987.
[PAUL89] L. Paulson, The foundation of a generic theorem prover, Journal of Automated Reasoning, 5(3), 1989, pp. 363-397.
[PAUL90] L. Paulson, Isabelle: the next 700 theorem provers, In: P. Odifreddi, editor, Logic and Computer Science, Academic Press, 1990.
[PAUL93] L. Paulson, Set theory for verication: I. From foundations to functions, Journal of Automated Reasoning, 11(3), 1993.
[PAUL94a] L. Paulson, A fixed point approach to implementing (co)inductive definitions, In: A. Bundy, editor, 12th International Conference on Automated Deduction - CADE-12, volume 814 of LNAI, Springer, 1994, pp. 148-161.
[PAUL94b] L. Paulson, T. Nipkow, Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer, 1994.
[PAUL95] L. Paulson, Set theory for verication: II. Induction and recursion, Journal of Automated Reasoning, 15(2), 1995.
[PAUL97] L. Paulson, Generic automatic proof tools, In: R. Vero, editor, Automated Reasoning and its Applications: Essays in Honor of Larry Wos, MIT Press, 1997.
[PAUL99] L. Paulson, A generic tableau prover and its integration with Isabelle, Journal of Universal Computer Science, 5(3), 1999.
[PAYN93] C. Payne, J. Froscher, C. Landwehr, Toward a comprehensive INFOSEC certification methodology, In: Proceedings of the 16th National Computer Security Conference, NIST/NSA, Baltimore, MD, September 1993, pp. 165-172.
[PAYN95] C. Payne, Secure Policy Model, Navy Handbook for the Computer Security Certification of Trusted Systems, Chapter 3, NRL Technical Memorandum NRL/TM/5540:080A. Naval Research Laboratory, Washington, DC. January 1995.
[PCCI97] President's Commission on Critical Infrastructure, Critical Foundations: Protecting America's Infrastructures, October 1997.
[PERI94] R. Peri, Specification and Verification of Security Policies, PhD thesis, the Faculty of the School of Engineering and Applied Science, University of Virginia, Charlottesville, VA, USA, 1994
[PICC87] J. Picciotto, The Design of An Effection Auditing Subsystem, In: IEEE Symposium on Security and Privacy, Oakland CA., 1987, pp.13-22.
[POVE99] D. Povey, Optimistic Security: A New Access Control Paradigm, In: ACM New Security Paradigm Workshop, Ontario, September 1999, Canada, pp.40-45.
[PRIC73] W. Price, Implications of a Virtual Memory Mechanism for Implementing Protection in a Family of Operating Systems, PhD thesis, Carnegie-Mellon University, June 1973.
[RAMA00] R. Ramakrishnan, J. Gehrke, Database Management Systems (2th ed.), McGraw-Hill, 2000, pp.51-83.
[REGE95] F. Regensburger, HOLCF: Higher order logic of computable functions, In: E. Schubert, P. Windley, J. Alves-Foss, editors, Higher Order Logic Theorem Proving and its Applications, volume 971 of LNCS, 1995.
[SAAL97] M. Saaltink. Domain checking Z specifications. In: C. Holloway, K. Hayhurst, editors, LFM' 97: Fourth NASA Langley Formal Methods Workshop, Hampton, VA, September 1997, pp. 185-192.
[SAMA00] P. Samarati, S. Vimercati, Access Control: Policies, Models, and Mechanisms, Revised versions of lectures given during the IFIP WG 1.7 International School on Foundations of Security Analysis and Design: Tutorial Lectures, September 01, 2000, pp.137-196.
[SAND88] R. Sandhu, Transaction Control Expressions for Separation of Duties, In: Fourth Aerospace Computer Security Applications Conference, Orland, Florida, 1988, pp.298-322.
[SAND95] R. Sandhu, Roles Versus Groups, In: Proceedings of the First ACM Workshop on Role-Based Access Control, Gaithersburg, Maryland, USA, December 1995, pp. 125-126.
[SAND96] R. Sandhu, E. Coyne, H. Feinstein, C. Youman, Role-Based Access Control Models, IEEE Computer, 29(2), February 1996, pp.38-47.
[SAND97] R. Sandhu, V. Bhamidipati, The ARBAC97 model for Role-based administration of Roles: Preliminary Description and Outline, In: Proceedings of second ACM Workshop on Role-Based Access Control, November 1997.
[SAND99a] R. Sandhu, V. Bhamidipati, Role-Based Administration of User-Role Assignment: The URA97 Model and its Oracle Implementation, Journal of Network and Computer Applications, 22(3), July 1999.
[SAND99b] R. Sandhu, Q. Munawer, The ARBAC99 Model for Administration of Roles, In: Proceedings of the 18' Annual Computer Security Applications Conference, Phoenix, Arizona, USA, December 1999, pp.229-238.
[SAYD89] O. Saydjari, J. Beckman, J. Leaman, LOCK trek: Navigating uncharted space, In: IEEE Symposium on Research in Security and Privacy, Oakland, CA, 1989, pp. 167-175.
[SCHA01] A. Schaad, J. Moffett, J. Jacob, The Role-Based Access Control System of a European Bank: A Case Study and Discussion, In: Proceedings of the 6th ACM Symposium on Access Control Models and Technologies, Litton-TASC, Chantilly, Virginia, USA, May 2001, pp. 3-9.
[SCHN99] F. Schneider (Ed.), Trust in Cyberspace, Committee on Information Systems trustworthiness, National Research Council, 1999.
[SEID90] K. Seiden, J. Melanson, The Auditing Facility for a VMM Security Kernel, In: IEEE Symposium on Security and Privacy, Oakland CA, May 1990, pp.2-19.
[SHAM79] A. Shamir, How to Share a Secret, Communications of the ACM, 22(11), November 1979, pp. 612-613
[SIHA01] 卿斯汉,刘文清,刘海峰,操作系统安全导论,北京:科学出版社,2001年1月.
[SIHA04a] 卿斯汉,刘文清,温红子,刘海峰,操作系统安全,北京:清华出版社,2004年7月.
[SIHA04b] 卿斯汉,温红子,雷浩,王建,基于Clark-Wilson完整性策略的安全监视模型,软件学报,Vol.15 NO.8,2004,pp.1124-1132.
[SIMO01] E Simone, IT-Security and Privacy, Berlin: Springer-Verlag, 2001.
[SLIN96] K. Slind, Function definition in higher order logic, In: J. Wright, J. Grundy, J. Harrison, editors, Theorem Proving in Higher Order Logics: TPHOLs '96, volume 1125 of LNCS, 1996.
[SLIN97] K. Slind, Derivation and use of induction schemes in higher-order logic, In: E. Gunter, A. Felty, editors, Theorem Proving in Higher Order Logics: TPHOLs '97, volume 1275 of LNCS, 1997.
[SMIT81] M. Smith, A. Siebert, B. Divito, D. Good, A Verified Encrypted Packet Interface, ACM Software Engineering Notes 6, 3, July 1981.
[SMIT88] B. Smith, C. Reese, K. Lindsay, B. Crane, A Description of a Formal Verification and Validation (FVV) Process, In: Proceedings of the 1988 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, August 1988, pp.401-408.
[SPIV93] J. Spivey, The fuzz Manual, Second edition, J. Spivey Computing Science Consultancy, May 1993.
[STER91] D. Sterne, On the buzzword "security policy", In: Proceedings Symposium on Research in Security and Privacy, IEEE, June 1991.
[THOM94] R. Thomas, R. Sandhu, Conceptual Foundations for a model of Task-Based Authorizations, In: Proceedings 7th Computer Security Foundations Workshop, IEEE CS Press, Los Alamitos, CA, June 1994, pp.66-79
[THOM97] R. Thomas, R. Sandhu, Task-Based Authorization Controls (TBAC): A Family of Models for Active and Enterprise-Oriented Autorization Management, In: Proceedings of the IFIP TC11 WG11.3 Eleventh International Conference on Database Seeurty Ⅺ: Status and Prospects, August 10-13, 1997, pp. 166-181.
[TOMA92] O. Tomas, A Structured Approach to Computer Security, Department of Computer Engineering, Chalmers University of Technology, Gothenburg, Technical Report No. 122, 1992.
[VIEN93] R. Vienneau, A Review of Formal Methods, Kaman Sciences Corporation, 1993.
[WEIS69] C. Weissman, Security Controls In The Adept-50 Time Sharing System, In: AFIPS Conference Proceedings, Fall Joint Computer Conference, Volume 35, 1969, pp. 119-133.
[WEIS70] C. Weissman, Trade-Off Considerations in Security System Design, SDC-SP 3548, September 10, 1970, also Data Management April 1972.
[WETS99] WetStone Technologies, Inc., Formal Methods Framework, final month status report, Contract # F30602-99-C-0166, October 26, 1999, available http://www.cs.utexas.edu/~csed/ FM/docs/FMFramework.pdf.
[WIED01] F. Wiedijk, Digital math WWW page, 2001. http://www.cs.kun.nl/~freek/ digimath/.
[WING90] J. Wing, A Specifier's Introduction to Formal Methods, IEEE Computer, Vol.23, No.9, September 1990, pp.8-23.
[WISE91] S. Wiseman, The Conflict between Confidentiality and Integrity, In: Proceedings 4th Workshop on the Foundations of Computer Security, IEEE Computer Society Press 1991, pp. 241-242.
[WOOD96] J. Woodcock, J. Davies, Using Z, Prentice Hall, 1996.
[ZEIG76] B. Zeigler, Theory of Modelling and Simulation, Wiley, New York, NY, 1976.
[ZHAN01] L. Zhang, G. Ahn, B. Chu, A Rule-Based Framework for Role-Based Delegation, In: Proceedings, of the 6th ACM Symposium on Access Control Models and Technologies, Litton-TASC, Chantilly, Virginia, USA, May 2001, pp. 153-162.