On Run-Time Enforcement of Authorization Constraints in Security-Sensitive Workflows

  • Daniel Ricardo dos SantosEmail author
  • Silvio Ranise
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10469)


In previous work, we showed how to use an SMT-based model checker to synthesize run-time enforcement mechanisms for business processes augmented with access control policies and authorization constraints, such as Separation of Duties. The synthesized enforcement mechanisms are able to guarantee both termination and compliance to security requirements, i.e. solving the run-time version of the Workflow Satisfiability Problem (WSP). No systematic approach to specify the various constraints considered in the WSP literature has been provided. In this paper, we first propose a classification of these constraints and then show how to encode them in the declarative input language of the SMT-based model checker used for synthesis. This shows the flexibility of the SMT approach to solve the run-time version of the WSP in presence of different authorization constraints.


  1. 1.
    Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Universal guards, relativization of quantifiers, and failure models in model checking modulo theories. JSAT 8, 29–61 (2012)MathSciNetzbMATHGoogle Scholar
  2. 2.
    Alhaqbani, B., Adams, M., Fidge, C.J., ter Hofstede, A.H.M.: Privacy-aware workflow management. In: Proceedings of BPM, pp. 111–128. Springer, Heidelberg (2013)Google Scholar
  3. 3.
    Basin, D., Burri, S.J., Karjoth, G.: Dynamic enforcement of abstract separation of duty constraints. TISSEC 15(3), 13:1–13:30 (2012)CrossRefGoogle Scholar
  4. 4.
    Basin, D., Burri, S.J., Karjoth, G.: Obstruction-free authorization enforcement: Aligning security and business objectives. JCS 22(5), 661–698 (2014)CrossRefGoogle Scholar
  5. 5.
    Bell, D.: The bell-lapadula model. JCS 4(2), 3 (1996)Google Scholar
  6. 6.
    Bertino, E., Ferrari, E., Atluri, V.: The specification and enforcement of authorization constraints in workflow management systems. TISSEC 2(1), 65–104 (1999)CrossRefGoogle Scholar
  7. 7.
    Bertolissi, C., dos Santos, D.R., Ranise, S.: Automated synthesis of run-time monitors to enforce authorization policies in business processes. In: Proceedings of ASIACCS. ACM (2015)Google Scholar
  8. 8.
    Biba, K.: Integrity considerations for secure computer systems. Technical report, DTIC Document (1977)Google Scholar
  9. 9.
    Brewer, D., Nash, M.J.: The Chinese wall security policy. In: Proceedings of S&P. IEEE (1989)Google Scholar
  10. 10.
    Burri, S.J, Karjoth, G.: Flexible scoping of authorization constraints on business processes with loops and parallelism. In: Proceedings of BPMW. Springer (2012)CrossRefGoogle Scholar
  11. 11.
    Cohen, D., Crampton, J., Gagarin, A., Gutin, G., Jones, M.: Iterative plan construction for the workflow satisfiability problem. JAIR 51, 555–577 (2014)MathSciNetzbMATHCrossRefGoogle Scholar
  12. 12.
    Cohen, D., Crampton, J., Gagarin, A., Gutin, G., Jones, M.: Algorithms for the workflow satisfiability problem engineered for counting constraints. J. Comb. Optim. 32(1), 3–24 (2016)MathSciNetzbMATHCrossRefGoogle Scholar
  13. 13.
    Compagna, L., dos Santos, D.R., Ponta, S.E., Ranise, S.: Cerberus: Automated synthesis of enforcement mechanisms for security-sensitive business processes. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 567–572. Springer, Heidelberg (2016). doi: 10.1007/978-3-662-49674-9_36CrossRefGoogle Scholar
  14. 14.
    Crampton, J.: A reference monitor for workflow systems with constrained task execution. In: Proceedings of SACMAT. ACM (2005)Google Scholar
  15. 15.
    Crampton, J., Gagarin, A., Gutin, G., Jones, M., Wahlström, M.: On the workflow satisfiability problem with class-independent constraints for hierarchical organizations. TOPS 19(3), 81–829 (2016)CrossRefGoogle Scholar
  16. 16.
    Crampton, J., Gutin, G.: Constraint expressions and workflow satisfiability. In: Proceedings of SACMAT. ACM (2013)Google Scholar
  17. 17.
    Crampton, J., Gutin, G., Yeo, A.: On the parameterized complexity and kernelization of the workflow satisfiability problem. TISSEC 16(1), 4 (2013)CrossRefGoogle Scholar
  18. 18.
    Crampton, J., Huth, M., Kuo, J.: Authorized workflow schemas: deciding realizability through LTL(F) model checking. STTT 16(1), 31–48 (2014)CrossRefGoogle Scholar
  19. 19.
    Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 53–68. Springer, Heidelberg (2000). doi: 10.1007/10722167_8zbMATHCrossRefGoogle Scholar
  20. 20.
    Dijkman, R.M., Dumas, M., Ouyang, C.: Semantics and analysis of business process models in BPMN. Inf. Soft. Tech. 50(12), 1281–1294 (2008)CrossRefGoogle Scholar
  21. 21.
    dos Santos, D.R., Ranise, S., Ponta, S.E.: Modular synthesis of enforcement mechanisms for the workflow satisfiability problem: scalability and reusability. In: Proceedings of SACMAT. ACM (2016)Google Scholar
  22. 22.
    Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. LMCS 6(4) (2010)Google Scholar
  23. 23.
    Ghilardi, S., Ranise, S.: MCMT: A model checker modulo theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 22–29. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-14203-1_3CrossRefGoogle Scholar
  24. 24.
    Leitner, M., Mangler, J., Rinderle-Ma, S.: Definition and enactment of instance-spanning process constraints. In: Wang, X.S., Cruz, I., Delis, A., Huang, G. (eds.) WISE 2012. LNCS, vol. 7651, pp. 652–658. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-35063-4_49CrossRefGoogle Scholar
  25. 25.
    Li, N., Wang, Q.: Beyond separation of duty: An algebra for specifying high-level security policies. J. ACM 55(3), 121–1246 (2008)MathSciNetzbMATHCrossRefGoogle Scholar
  26. 26.
    Nassr, N., Steegmans, E.: Mitigating conflicts of interest by authorization policies. In: Proceedings of SIN. ACM (2015)Google Scholar
  27. 27.
    Sandhu, R., Coyne, E., Feinstein, H., Youmann, C.: Role-based access control models. IEEE Comput. 2(29), 38–47 (1996)CrossRefGoogle Scholar
  28. 28.
    Sankaranarayanan, S., Sipma, H., Manna, Z.: Petri net analysis using invariant generation. In: Verification: Theory and Practice. Springer (2003)Google Scholar
  29. 29.
    Tan, K., Crampton, J., Gunter, C.A.: The consistency of task-based authorization constraints in workflow. In Proceedings of CSF. IEEE (2004)Google Scholar
  30. 30.
    van der Aalst, W.M.P., van Hee, K.M., ter Hofstede, A.H.M., Sidorova, N., Verbeek, H.M.W., Voorhoeve, M., Wynn, M.T.: Soundness of workflow nets: classification, decidability, and analysis. Formal Aspects Comp. 23(3), 333–363 (2011)MathSciNetzbMATHCrossRefGoogle Scholar
  31. 31.
    Wang, Q., Li, N.: Satisfiability and resiliency in workflow authorization systems. TISSEC 13(4), 401–4035 (2010)MathSciNetCrossRefGoogle Scholar
  32. 32.
    Warner, J., Atluri, V.: Inter-instance authorization constraints for secure workflow management. In: Proceedings of SACMAT (2006). ACMGoogle Scholar
  33. 33.
    Wolter, C., Schaad, A., Meinel, C.: Task-based entailment constraints for basic workflow patterns. ACM, In Proc. of SACMAT (2008)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Fondazione Bruno Kessler (FBK)TrentoItaly

Personalised recommendations