Analysis and Run-Time Verification of Dynamic Security Policies

  • Helge Janicke
  • François Siewe
  • Kevin Jones
  • Antonio Cau
  • Hussein Zedan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3890)


Ensuring the confidentiality, integrity and availability of information is the key issue in the battle for information superiority and thus is a decisive factor in modern warfare. Security policies and security mechanisms govern the access to information and other resources. Their correct specification, i.e. denial of potentially dangerous access and adherence to all established need-to-know requirements, is critical. In this paper we present a security model that allows to express dynamic access control policies that can change on time or events. A simple agent system, simulating a platoon, is used to show the need and the advantages of our policy model. The paper finally presents how existing tool-support can be used for the analysis and verification of policies.


Access Control Security Policy Security Requirement Security Model Access Control Policy 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Thomas, E., Potok, A.S.L., Phillips, L., Pollock, R.: Suitability of agent technology or military command and control in the future combat system environment. In: Proceeding 8th ICCRTS, National Defence University (2003)Google Scholar
  2. 2.
    Sheldon, F., Potok, T., Kavi, K.: Multi-agent system case studies in command and control, information fusion and data management. Journal of Informatica 28, 78–89 (2004)zbMATHGoogle Scholar
  3. 3.
    Bharadwajgc, R.: Secure middleware for situation-aware naval c2 and combat systems. In: Proceedings 9th International Workshop on Future Trends of Distributed Comput ing Systems, FTDCS 2003 (2003)Google Scholar
  4. 4.
    Alberts, D.S.: Understanding information age warfare. CCRP publication series. DoD, US (2001)Google Scholar
  5. 5.
    Jajodia, S., Samarati, P., Subrahmanian, V.S., Bertino, E.: A unified framework for enforcing multiple access control policies. ACM Transaction on Database Systems 26, 214–260 (2001)CrossRefzbMATHGoogle Scholar
  6. 6.
    Abadi, M., Burrows, M., Lampson, B., Plotkin, G.: A calculus for access control in distributed systems. ACM Transactions on Programming Languages and Systems  15, 1–29 (1993)CrossRefGoogle Scholar
  7. 7.
    Barker, S., Stuckey, P.J.: Flexible access control specification with constraint logic programming. ACM Transactions on Information & System Security 6 (2003)Google Scholar
  8. 8.
    Bertino, E., Bonatti, P.A., Ferrari, E.: Trbac: A temporal role-based access control model. ACM Trans. Inf. Syst. Secur. 4, 191–233 (2001)CrossRefGoogle Scholar
  9. 9.
    Cau, A., Czarnecki, C., Zedan, H.: Designing a provably correct robot control system using a ‘Lean’ formal method. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 123–132. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  10. 10.
    Siewe, F., Cau, A., Zedan, H.: A compositional framework for access control policies enforcement. In: Proceedings of the ACM workshop on Formal Methods in Security Engineering: From Specifications to Code (2003)Google Scholar
  11. 11.
    Eckert, C.: Matching security to application needs. In: IFIP TC11 11th International Conference on Information Security, pp. 237–254 (1995)Google Scholar
  12. 12.
    Moszkowski, B.: Some very compositional temporal properties. In: Olderog, E.R. (ed.) Programming Concepts, Methods and Calculi. IFIP Transactions, vol. A-56, pp. 307–326. IFIP, Elsevier Science B.V., North-Holland (1994)Google Scholar
  13. 13.
    Zedan, H., Cau, A., Zhou, S.: A calculus for evolution. In: Proc. of The Fifth International Conference on Computer Science and Informatics, CS&I 2000 (2000)Google Scholar
  14. 14.
    Woo, T.Y.C., Lam, S.S.: Authorization in distributed systems: A formal approach. In: Proceedings of the 13th IEEE Symposium on Research in security and Privacy, Oakland, California, May 4-6, pp. 33–50 (1992)Google Scholar
  15. 15.
    Brewer, D., Nash, M.: The Chinese Wall Policy. In: IEEE Symposium on Research in Security and Privacy, pp. 206–214 (1989)Google Scholar
  16. 16.
    Moszkowski, B.: Executing Temporal Logic Programs. Cambridge University Press, England (1986)zbMATHGoogle Scholar
  17. 17.
    Cau, A., Moszkowski, B., Zedan, H.: The ITL homepage (2005),
  18. 18.
    Fisher, M.: A survey of concurrent METATEM – the language and its applications. In: Gabbay, D.M., Ohlbach, H.J. (eds.) ICTL 1994. LNCS (LNAI), vol. 827, pp. 480–505. Springer, Heidelberg (1994)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Helge Janicke
    • 1
  • François Siewe
    • 1
  • Kevin Jones
    • 1
  • Antonio Cau
    • 1
  • Hussein Zedan
    • 1
  1. 1.Software Technology Research Laboratory, Gateway HouseDe Montfort UniversityLeicesterUK

Personalised recommendations