Model Checking Usage Policies

  • Massimo Bartoletti
  • Pierpaolo Degano
  • Gian Luigi Ferrari
  • Roberto Zunino
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5474)


We propose a model for specifying, analysing and enforcing safe usage of resources. Our usage policies allow for parametricity over resources, and they can be enforced through finite state automata. The patterns of resource access and creation are described through a basic calculus of usages. In spite of the augmented flexibility given by resource creation and by policy parametrization, we devise an efficient (polynomial-time) model-checking technique for deciding when a usage is resource-safe, i.e. when it complies with all the relevant usage policies.


Model Check Security Policy State Automaton Covert Channel Usage 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.
    Abadi, M., Fournet, C.: Access control based on execution history. In: Proc. 10th Annual Network and Distributed System Security Symposium (2003)Google Scholar
  2. 2.
    Acciai, L., Boreale, M.: Spatial and behavioral types in the π-calculus. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 372–386. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  3. 3.
    Bartoletti, M., Degano, P., Ferrari, G.L.: Static analysis for stack inspection. In: International Workshop on Concurrency and Coordination (2001)Google Scholar
  4. 4.
    Bartoletti, M., Degano, P., Ferrari, G.L.: History-based access control with local policies. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 316–332. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Bartoletti, M., Degano, P., Ferrari, G.L.: Types and effects for secure service orchestration. In: Proc. 19th CSFW (2006)Google Scholar
  6. 6.
    Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Types and effects for resource usage analysis. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 32–47. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Model checking usage policies. Technical Report TR-08-06, Dip. Informatica, Univ. Pisa (2008)Google Scholar
  8. 8.
    Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Semantics-based design for secure web services. IEEE Transactions on Software Engineering 34(1) (2008)Google Scholar
  9. 9.
    Bartoletti, M., Zunino, R.: LocUsT: a tool for checking usage policies. Technical Report TR-08-07, Dip. Informatica, Univ. Pisa (2008)Google Scholar
  10. 10.
    Bauer, L., Ligatti, J., Walker, D.: More enforceable security policies. In: Foundations of Computer Security (FCS) (2002)Google Scholar
  11. 11.
    Bauer, L., Ligatti, J., Walker, D.: Composing security policies with Polymer. In: Proc. PLDI (2005)Google Scholar
  12. 12.
    Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theoretical Computer Science 37, 77–121 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Brewer, D.F.C., Nash, M.J.: The chinese wall security policy. In: Proc. of Symp. on Security and Privacy (1989)Google Scholar
  14. 14.
    Bruni, R., Mezzina, L.G.: Types and deadlock freedom in a calculus of services, sessions and pipelines. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 100–115. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  15. 15.
    Caires, L., Vieira, H.T.: Typing conversations in the conversation calculus. Technical Report 3/08, DI/FCT/UNL (2008)Google Scholar
  16. 16.
    Christensen, S.: Decidability and Decomposition in Process Algebras. PhD thesis, Edinburgh University (1993)Google Scholar
  17. 17.
    Colcombet, T., Fradet, P.: Enforcing trace properties by program transformation. In: Proc. 27th ACM SIGPLAN-SIGACT PoPL (2000)Google Scholar
  18. 18.
    Erlingsson, Ú., Schneider, F.B.: SASI enforcement of security policies: a retrospective. In: Proc. 7th New Security Paradigms Workshop (1999)Google Scholar
  19. 19.
    Esparza, J.: On the decidability of model checking for several μ-calculi and Petri nets. In: Tison, S. (ed.) CAAP 1994. LNCS, vol. 787. Springer, Heidelberg (1994)Google Scholar
  20. 20.
    Fong, P.W.: Access control by tracking shallow execution history. In: IEEE Symposium on Security and Privacy (2004)Google Scholar
  21. 21.
    Igarashi, A., Kobayashi, N.: Type reconstruction for linear -calculus with i/o subtyping. Inf. Comput. 161(1), 1–44 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Igarashi, A., Kobayashi, N.: Resource usage analysis. In: Proc. 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2002)Google Scholar
  23. 23.
    Jalapa: Securing Java with Local Policies,
  24. 24.
    Marriott, K., Stuckey, P.J., Sulzmann, M.: Resource usage verification. In: Proc. First Asian Programming Languages Symposium (2003)Google Scholar
  25. 25.
    Mayr, R.: Decidability and Complexity of Model Checking Problems for Infinite-State Systems. PhD thesis, Technischen Universität München (1998)Google Scholar
  26. 26.
    Thiemann, P.: Enforcing safety properties using type specialization. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, p. 62. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  27. 27.
    Wang, J., Takata, Y., Seki, H.: HBAC: A model for history-based access control and its model checking. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 263–278. Springer, Heidelberg (2006)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Massimo Bartoletti
    • 1
    • 2
  • Pierpaolo Degano
    • 2
  • Gian Luigi Ferrari
    • 2
  • Roberto Zunino
    • 3
  1. 1.Dipartimento di Matematica e InformaticaUniversità degli Studi di CagliariItaly
  2. 2.Dipartimento di InformaticaUniversità di PisaItaly
  3. 3.Dipartimento di Ingegneria e Scienza dell’InformazioneUniversità di TrentoItaly

Personalised recommendations