Security Validation of Business Processes via Model-Checking

  • Wihem Arsac
  • Luca Compagna
  • Giancarlo Pellegrino
  • Serena Elisa Ponta
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6542)


More and more industrial activities are captured through Business Processes (BPs). To evaluate whether a BP under-design enjoys certain security desiderata is hardly manageable by business analysts without tool support, as the BP runtime environment is highly dynamic (e.g., task delegation). Automated reasoning techniques such as model checking can provide the required level of assurance but suffer of well-known obstacles for the adoption in industrial systems, e.g. they require a strong logical and mathematical background. In this paper, we present a novel security validation approach for BPs that employs state-of-the-art model checking techniques for evaluating security-relevant aspects of BPs in dynamic environments and offers accessible user interfaces and apprehensive feedback for business analysts so to be suitable for industry.


Business Process Model Check Business Process Management Horn Clause 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.
    Clarke, E.M., Grumberg, O., Peled, D.: Model checking (2000)Google Scholar
  2. 2.
    Karch, S., Heilig, L.: SAP NetWeaver, 1. aufl edn. Galileo Press, Bonn (2004)Google Scholar
  3. 3.
    Sandhu, R.S., Coyne, E.J., Feinstein, H.L., Youman, C.E.: Role-based access control models. Computer 29(2), 38–47 (1996)CrossRefGoogle Scholar
  4. 4.
    Giorgini, P., Massacci, F., Mylopoulos, J.: Modeling security requirements through ownership, permission and delegation. In: RE, pp. 167–176. IEEE Press, Los Alamitos (2005)Google Scholar
  5. 5.
    AVANTSSAR: Deliverable 2.1: Requirements for modelling and ASLan v.1 (2008),
  6. 6.
    Armando, A., Carbone, R., Compagna, L.: LTL Model Checking for Security Protocols. In: JANCL, Special Issue on Logic and Information Security (2009)Google Scholar
  7. 7.
    Schaad, A., Lotz, V., Sohr, K.: A model-checking approach to analysing organisational controls in a loan origination process. In: SACMAT, pp. 139–149. ACM, New York (2006)CrossRefGoogle Scholar
  8. 8.
    Wolter, C., Miseldine, P., Meinel, C.: Verification of business process entailment constraints using SPIN. In: Massacci, F., Redwine Jr., S.T., Zannone, N. (eds.) ESSoS 2009. LNCS, vol. 5429, pp. 1–15. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  9. 9.
    Rakkay, H., Boucheneb, H.: Security analysis of role based access control models using colored petri nets and cpntools, pp. 149–176 (2009)Google Scholar
  10. 10.
    Zhang, N., Ryan, M., Guelev, D.P.: Evaluating access control policies through model checking. In: Zhou, J., López, J., Deng, R.H., Bao, F. (eds.) ISC 2005. LNCS, vol. 3650, pp. 446–460. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  11. 11.
    Teepe, W., van de Riet, R., Olivier, M.: Workflow analyzed for security and privacy in using databases. J. Comput. Secur. 11(3), 353–363 (2003)CrossRefzbMATHGoogle Scholar
  12. 12.
    Awad, A., Weidlich, M., Weske, M.: Specification, verification and explanation of violation for data aware compliance rules. In: ICSOC-Service Wave (2009)Google Scholar
  13. 13.
    Jan, J.: Secure Systems Development with UML. Springer Academic Publishers, Heidelberg (2005)zbMATHGoogle Scholar
  14. 14.
    Höhn, S., Jürjens, J.: Rubacon: automated support for model-based compliance engineering. In: ICSE, pp. 875–878 (2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Wihem Arsac
    • 1
  • Luca Compagna
    • 1
  • Giancarlo Pellegrino
    • 1
  • Serena Elisa Ponta
    • 1
    • 2
  1. 1.SAP Research Sophia-AntipolisMouginsFrance
  2. 2.U. of GenovaGenovaItaly

Personalised recommendations