A tool for the synthesis of cryptographic orchestrators

ABSTRACT

Security is one of the main challenges of service oriented computing. Services need to be loosely coupled, easily accessible and yet provide tight security guarantees enforced by cryptographic protocols. In this paper, we address how to automatically synthesize an orchestrator process able to guarantee the secure composition of electronic services, supporting different communication and cryptographic protocols. We present a theoretical model based on process algebra, partial model checking and logical satisfiability, plus an automated tool implementing the proposed theory.

References

1. PaMoChSA 2012. http://www.iit.cnr.it/staff/vincenzo.ciancia/tools.html.
2. H. R. Andersen. Partial model checking. In LICS, page 398. IEEE, 1995.
3. Y. Chevalier, M. A. Mekki, and M. Rusinowitch. Automatic composition of services with security policies. In SERVICES'08 - Part I, pages 529--537. IEEE, 2008.
4. J. Li, M. Yarvis, and P. Reiher. Securing distributed adaptation. Computer Networks, 38(3), 2002.
5. O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers for timed systems. In STACS, volume 900 of LNCS, pages 229--242. Springer, 2005.
6. J. A. Martín, F. Martinelli, and E. Pimentel. Synthesis of secure adaptors. J. Log. Algebr. Program., 81(2):99--126, 2012.
7. J. A. Martín and E. Pimentel. Contracts for security adaptation. J. Log. Algebr. Program., 80(3--5):154--179, 2011.
8. F. Martinelli. Analysis of security protocols as open systems. TCS, 290(1):1057--1106, 2003.
9. F. Martinelli and I. Matteucci. A framework for automatic generation of security controller. STVR, 2010.
10. F. Martinelli, M. Petrocchi, and A. Vaccarelli. Automated analysis of some security mechanisms of SCEP. In ISC, pages 414--427. Springer, 2002.
11. R. Milner. Communication and concurrency. Prentice-Hall, 1989.
12. C. Stirling. Modal and temporal logics for processes. In Logics for Concurrency: Structures versus Automata, pages 149--237, 1996.
13. R. S. Streett and E. A. Emerson. An automata theoretic decision procedure for the propositional mu-calculus. Information and Computation, 81(3):249--264, June 1989.
14. L. Viganò. Automated security protocol analysis with the AVISPA tool. ENTCS, 155:69--86, 2006.

Index Terms

• Information systems

  • Data management systems

    • Data structures

      • Data layout

        • Data encryption

• Security and privacy

  • Cryptography

  • Systems security

    • Operating systems security

• Software and its engineering

  • Software creation and management

    • Designing software

      • Software implementation planning

        • Software design techniques

    • Software development process management

• Theory of computation

  • Computational complexity and cryptography