References of "Chevalier, Yannick"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailTowards the Orchestration of Secured Services under Non-disclosure Policies
Avanesov, Tigran UL; Chevalier, Yannick; Rusinowitch, Michaël et al

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 (2012)

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 ... [more ▼]

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. [less ▲]

Detailed reference viewed: 109 (6 UL)
Full Text
Peer Reviewed
See detailThe AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures
Armando, Alessandro; Arsac, Wihem; Avanesov, Tigran UL et al

in Proceedings of 18th International Conference "Tools and Algorithms for the Construction and Analysis of Systems", as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. (2012)

The AVANTSSAR Platform is an integrated toolset for the formal specification and automated validation of trust and security of service-oriented architectures and other applications in the Internet of ... [more ▼]

The AVANTSSAR Platform is an integrated toolset for the formal specification and automated validation of trust and security of service-oriented architectures and other applications in the Internet of Services. The platform supports application-level specification languages (such as BPMN and our custom languages) and features three validation backends (CL-AtSe, OFMC, and SATMC), which provide a range of complementary automated reasoning techniques (including service orchestration, compositional reasoning, model checking, and abstract interpretation). We have applied the platform to a large number of industrial case studies, collected into the AVANTSSAR Library of validated problem cases. In doing so, we unveiled a number of problems and vulnerabilities in deployed services. These include, most notably, a serious flaw in the SAML-based Single Sign-On for Google Apps (now corrected by Google as a result of our findings). We also report on the migration of the platform to industry. [less ▲]

Detailed reference viewed: 129 (5 UL)
Full Text
Peer Reviewed
See detailDistributed Orchestration of Web Services under Security Constraints
Avanesov, Tigran UL; Chevalier, Yannick; Anis Mekki, Mohammed et al

in Data Privacy Management and Autonomous Spontaneus Security - 6th International Workshop, DPM 2011, and 4th International Workshop, SETOP 2011, Leuven, Belgium, September 15-16, 2011, Revised Selected Papers. (2011)

We present a novel approach to automated distributed orchestration of Web services tied with security policies. The construction of an orchestration complying with the policies is based on the resolution ... [more ▼]

We present a novel approach to automated distributed orchestration of Web services tied with security policies. The construction of an orchestration complying with the policies is based on the resolution of deducibility constraint systems and has been implemented for the non-distributed case as part of the AVANTSSAR Validation Platform. The tool has been successfully experimented on several case-studies from industry and academia. [less ▲]

Detailed reference viewed: 134 (0 UL)
Full Text
Peer Reviewed
See detailWeb Services Verification and Prudent Implementation
Avanesov, Tigran UL; Chevalier, Yannick; Anis Mekki, Mohammed et al

in Data Privacy Management and Autonomous Spontaneus Security - 6th International Workshop, DPM 2011, and 4th International Workshop, SETOP 2011, Leuven, Belgium, September 15-16, 2011, Revised Selected Papers. (2011)

Alice&Bob notation is widely used to describe conversations between partners in security protocols. We present a tool that compiles an Alice&Bob description of a Web Services choreography into a set of ... [more ▼]

Alice&Bob notation is widely used to describe conversations between partners in security protocols. We present a tool that compiles an Alice&Bob description of a Web Services choreography into a set of servlets. For that we first compute for each partner an executable specification as prudent as possible of her role in the choreography. This specification is expressed in ASLan language, a formal language designed for modeling Web Services tied with security policies. Then we can check with automatic tools that this ASLan specification verifies some required security properties such as secrecy and authentication. If no flaw is found, we compile the specification into Java servlets that real partners can use to execute the choreography. [less ▲]

Detailed reference viewed: 129 (1 UL)
Full Text
Peer Reviewed
See detailSatisfiability of general intruder constraints with a set constructor
Avanesov, Tigran UL; Chevalier, Yannick; Rusinowitch, Michael et al

in CRiSIS 2010, Proceedings of the Fifth International Conference on Risks and Security of Internet and Systems, Montreal, QC, Canada, October 10-13, 2010. (2010)

Many decision problems on security protocols can be reduced to solving so-called intruder constraints in Dolev Yao model. Most constraint solving procedures for protocol security rely on two properties of ... [more ▼]

Many decision problems on security protocols can be reduced to solving so-called intruder constraints in Dolev Yao model. Most constraint solving procedures for protocol security rely on two properties of constraint systems called monotonicity and variable-origination. In this work we relax these restrictions by giving an NP decision procedure for solving general intruder constraints (that do not have these properties). Our result extends a first work by L. Mazaré in several directions: we allow non-atomic keys, and an associative, commutative and idempotent symbol (for modeling sets). We also give several new applications of the result. [less ▲]

Detailed reference viewed: 101 (4 UL)