2012 • In 6th International Conference on Mathematical Methods, Models and Architectures for Computer Network Security, MMM-ACNS 2012, St. Petersburg, Russia, October 17-19, 2012. Proceedings
Web services; Orchestration; security policy; separation of duty; deducibility constraints; cryptographic protocols
Résumé :
[en] 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.
Disciplines :
Sciences informatiques
Identifiants :
UNILU:UL-CONFERENCE-2012-390
Auteur, co-auteur :
AVANESOV, Tigran ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
Chevalier, Yannick; IRIT, Université de Toulouse, France
Rusinowitch, Michaël; INRIA Nancy Grand Est, France
Turuani, Mathieu; INRIA Nancy Grand Est, France
Langue du document :
Anglais
Titre :
Towards the Orchestration of Secured Services under Non-disclosure Policies
Date de publication/diffusion :
2012
Nom de la manifestation :
6th International Conference on Mathematical Methods, Models and Architectures for Computer Network Security, MMM-ACNS 2012
Lieu de la manifestation :
St. Petersburg, Russie
Date de la manifestation :
Oct 17, 2012 - Oct 20, 2012
Titre de l'ouvrage principal :
6th International Conference on Mathematical Methods, Models and Architectures for Computer Network Security, MMM-ACNS 2012, St. Petersburg, Russia, October 17-19, 2012. Proceedings
Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 367(1-2), 2-32 (2006) (Pubitemid 44649345)
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)
Avanesov, T., Chevalier, Y., Rusinowitch, M., Turuani, M.: Satisfiability of general intruder constraints with and without a set constructor. CoRR, abs/1103.0220 (2011)
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), http://hal.inria.fr/ hal-00719011
Automated Validation of Trust and Security of Service-Oriented Architectures, AVANTSSAR project, http://www.avantssar.eu
Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Proceedings of CCS 2005 Conference, pp. 16-25. ACM (2005) (Pubitemid 44021986)
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)
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) (Pubitemid 44753720)
Costa, G., Degano, P., Martinelli, F.: Secure service orchestration in open networks. Journal of Systems Architecture - Embedded Systems Design 57(3), 231-239 (2011)
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198-208 (1983)
Armando, A., Arsac, W., Avanesov, T., Barletta, M., Calvi, A., Cappai, A., Carbone, R., Chevalier, Y., Compagna, L., Cúellar, 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)
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)
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)
Kourjieh, M.: Logical Analysis and Verification of Cryptographic Protocols. Thèse de doctorat, Université Paul Sabatier, Toulouse, France, (Décembre 2009)
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)
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)
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), http://profs.sci.univr.it/~vigano/fcs- arspa07/fcs-arspa07.pdf (Pubitemid 40276660)
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) (Pubitemid 41422037)
McAllester, D.A.: Automatic recognition of tractability in inference relations. Journal of the ACM 40, 284-303 (1993)
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) (Pubitemid 34974717)
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) (Pubitemid 34974717)
Network of Excellence on Engineering Secure Future Internet Software Services and Systems, NESSoS project, http://www.nessos-project.eu
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)
Turuani, M.: The CL-Atse Protocol Analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 277-286. Springer, Heidelberg (2006) (Pubitemid 44502673)
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)
