Towards the Orchestration of Secured Services under Non-disclosure Policies

  • Tigran Avanesov
  • Yannick Chevalier
  • Michaël Rusinowitch
  • Mathieu Turuani
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7531)


The problem of finding a mediator to compose secured services has been reduced in our former work to the problem of solving deducibility constraints similar to those employed for cryptographic protocol analysis. We extend in this paper the mediator synthesis procedure by a construction for expressing that some data is not accessible to the mediator. Then we give a decision procedure for verifying that a mediator satisfying this non-disclosure policy can be effectively synthesized. This procedure has been implemented in CL-AtSe, our protocol analysis tool. The procedure extends constraint solving for cryptographic protocol analysis in a significative way as it is able to handle negative deducibility constraints without restriction. In particular it applies to all subterm convergent theories and therefore covers several interesting theories in formal security analysis including encryption, hashing, signature and pairing.


Web services Orchestration security policy separation of duty deducibility constraints cryptographic protocols 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 367(1-2), 2–32 (2006)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Avanesov, T., Chevalier, Y., Mekki, M.A., Rusinowitch, M.: Web Services Verification and Prudent Implementation. In: Garcia-Alfaro, J., Navarro-Arribas, G., Cuppens-Boulahia, N., de Capitani di Vimercati, S. (eds.) DPM 2011 and SETOP 2011. LNCS, vol. 7122, pp. 173–189. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  3. 3.
    Avanesov, T., Chevalier, Y., Rusinowitch, M., Turuani, M.: Satisfiability of general intruder constraints with and without a set constructor. CoRR, abs/1103.0220 (2011)Google Scholar
  4. 4.
    Avanesov, T., Chevalier, Y., Rusinowitch, M., Turuani, M.: Intruder deducibility constraints with negation. Decidability and application to secured service compositions. INRIA Research Report (July 2012),
  5. 5.
    Automated Validation of Trust and Security of Service-Oriented Architectures, AVANTSSAR project,
  6. 6.
    Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Proceedings of CCS 2005 Conference, pp. 16–25. ACM (2005)Google Scholar
  7. 7.
    Chevalier, Y., Mekki, M.A., Rusinowitch, M.: Automatic composition of services with security policies. In: Proceedings of SERVICES I 2008, SERVICES 2008. pp. 529–537. IEEE, Washington, DC (2008)Google Scholar
  8. 8.
    Corin, R., Etalle, S., Saptawijaya, A.: A logic for constraint-based security protocol analysis. In: IEEE Symposium on Security and Privacy (S&P), Berkeley, California, USA, May 21-24, pp. 155–168. IEEE Computer Society (2006)Google Scholar
  9. 9.
    Costa, G., Degano, P., Martinelli, F.: Secure service orchestration in open networks. Journal of Systems Architecture - Embedded Systems Design 57(3), 231–239 (2011)Google Scholar
  10. 10.
    Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)MathSciNetzbMATHCrossRefGoogle Scholar
  11. 11.
    Armando, A., Arsac, W., Avanesov, T., Barletta, M., Calvi, A., Cappai, A., Carbone, R., Chevalier, Y., Compagna, L., Cuéllar, J., Erzse, G., Frau, S., Minea, M., Mödersheim, S., von Oheimb, D., Pellegrino, G., Ponta, S.E., Rocchetto, M., Rusinowitch, M., Torabi Dashti, M., Turuani, M., Viganò, L.: The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 267–282. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  12. 12.
    Frau, S., Torabi Dashti, M.: Integrated specification and verification of security protocols and policies. In: 24th IEEE Computer Security Foundations Symposium, CSF 2011, Cernay-la-Ville, France, June 27-29, pp. 18–32 (2011)Google Scholar
  13. 13.
    Herzig, A., Lorini, E., Hübner, J.F., Vercouter, L.: A logic of trust and reputation. Logic Journal of IGPL 18(1), 214–244 (2010)zbMATHCrossRefGoogle Scholar
  14. 14.
    Kourjieh, M.: Logical Analysis and Verification of Cryptographic Protocols. Thèse de doctorat, Université Paul Sabatier, Toulouse, France, (Décembre 2009)Google Scholar
  15. 15.
    Kourjhler, D., Ksters, R., Truderung, T.: Infinite state amc-model checking for cryptographic protocols. In: Symposium on Logic in Computer Science, pp. 181–192 (2007)Google Scholar
  16. 16.
    Lorini, E., Demolombe, R.: Trust and Norms in the Context of Computer Security: A Logical Formalization. In: van der Meyden, R., van der Torre, L. (eds.) DEON 2008. LNCS (LNAI), vol. 5076, pp. 50–64. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  17. 17.
    Lynch, C., Meadows, C.: On the relative soundness of the free algebra model for public key encryption. In: Proceedings of the 2007 FCS-ARSPA Workshop. ENTCS, vol. 125, pp. 43–54 (2005),
  18. 18.
    Martinelli, F.: Towards an Integrated Formal Analysis for Security and Trust. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, pp. 115–130. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  19. 19.
    McAllester, D.A.: Automatic recognition of tractability in inference relations. Journal of the ACM 40, 284–303 (1993)MathSciNetzbMATHCrossRefGoogle Scholar
  20. 20.
    Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proceedings of the 8th ACM Conference on Computer and Communications Security, CCS 2001, pp. 166–175. ACM, New York (2001)CrossRefGoogle Scholar
  21. 21.
    Millen, J.K., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proceedings of the ACM Conference on Computer and Communications Security CCS 2001, pp. 166–175 (2001) Google Scholar
  22. 22.
    Network of Excellence on Engineering Secure Future Internet Software Services and Systems, NESSoS project,
  23. 23.
    Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: Proceedings of CSFW 2001, pp. 174–190. IEEE Computer Society Press (2001)Google Scholar
  24. 24.
    Turuani, M.: The CL-Atse Protocol Analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 277–286. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  25. 25.
    Chevalier, Y., Mekki, M.A., Rusinowitch, M.: Orchestration under Security Constraints. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 23–44. Springer, Heidelberg (2011)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Tigran Avanesov
    • 1
    • 2
    • 3
  • Yannick Chevalier
    • 2
  • Michaël Rusinowitch
    • 1
  • Mathieu Turuani
    • 1
  1. 1.INRIA Nancy Grand EstVandœuvre-lés-NancyFrance
  2. 2.IRITUniversité de ToulouseToulouseFrance
  3. 3.SnTUniversité du LuxebmourgLuxembourgLuxembourg

Personalised recommendations