We show how to model service-oriented applications using the process algebra CaPiTo so that, on the one hand, we can achieve an abstract specification without being overwhelmed by the underlying implementation details and, on the other hand, we can obtain a concrete specification respecting the industrial standards used for ensuring security. We consider this development important in order to get a good agreement between the protocols analysed by formal tools and the applications developed by practitioners. We then show how to transform the concrete specification into the LySa analysis framework, used in the SENSORIA EU project and originally developed in the DEGAS EU project, for analysing cryptographic protocols under a Dolev-Yao attacker. This allows us to perform a control flow analysis for ensuring the authenticity (as well as confidentiality) of messages exchanged between services. The LySa analysis framework is implemented in polynomial time in the size of the protocol specification using the Succinct Solver, that can solve a superset of Datalog clauses.
CITATION STYLE
Nielson, F., Gao, H., & Nielson, H. R. (2010). The CaPiTo approach to protocol validation: (Invited Talk). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6186 LNCS, p. 1). Springer Verlag. https://doi.org/10.1007/978-3-642-16074-5_1
Mendeley helps you to discover research relevant for your work.