The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures
Identifieur interne : 004A90 ( Hal/Curation ); précédent : 004A89; suivant : 004A91The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures
Auteurs : Alessandro Armando [France] ; Wihem Arsac [France] ; Tigran Avanesov [France] ; Michele Barletta [Italie] ; Alberto Calvi [Italie] ; Alessandro Cappai [France] ; Roberto Carbone [France] ; Yannick Chevalier [France] ; Luca Compagna [France] ; Jorge Cuellar [Allemagne] ; Gabriel Erzse [Roumanie] ; Simone Frau [Suisse] ; Marius Minea [Roumanie] ; Sebastian Modersheim [France] ; David Von Oheimb [Allemagne] ; Giancarlo Pellegrino [France] ; Serena Elisa Ponta [France] ; Marco Rocchetto [Italie] ; Michaël Rusinowitch [France] ; Mohammad Torabi Dashti [Suisse] ; Mathieu Turuani [France] ; Luca Vigano [Italie]Source :
Abstract
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.
Url:
DOI: 10.1007/978-3-642-28756-5_19
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: Pour aller vers cette notice dans l'étape Curation :004A90
Links to Exploration step
Hal:hal-00759725Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures</title><author><name sortKey="Armando, Alessandro" sort="Armando, Alessandro" uniqKey="Armando A" first="Alessandro" last="Armando">Alessandro Armando</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-135086" status="VALID"><orgName>Dipartimento di Informatica, Sistemistica e Telematica</orgName><orgName type="acronym">DIST</orgName><desc><address><addrLine>Dipartimento di Informatica, Sistemistica e Telematica Viale F. Causa, 13 16145 GENOVA - ITALIA</addrLine><country key="FR"></country></address><ref type="url">http://www.dist.unige.it/</ref></desc><listRelation><relation active="#struct-301142" type="direct"></relation><relation active="#struct-366388" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-301142" type="direct"><org type="institution" xml:id="struct-301142" status="VALID"><orgName>University of Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-366388" type="direct"><org type="institution" xml:id="struct-366388" status="INCOMING"><orgName>Università di Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Arsac, Wihem" sort="Arsac, Wihem" uniqKey="Arsac W" first="Wihem" last="Arsac">Wihem Arsac</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-132970" status="VALID"><orgName>SAP Research [Sophia Antipolis]</orgName><desc><address><addrLine>805 Avenue du Docteur Maurice Donat, BP1216-06254 Mougins, France</addrLine><country key="FR"></country></address></desc><listRelation><relation active="#struct-301537" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-301537" type="direct"><org type="institution" xml:id="struct-301537" status="VALID"><orgName>SAP Research</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Avanesov, Tigran" sort="Avanesov, Tigran" uniqKey="Avanesov T" first="Tigran" last="Avanesov">Tigran Avanesov</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-189789" status="VALID"><idno type="RNSR">200318302K</idno><orgName>Combination of approaches to the security of infinite states systems</orgName><orgName type="acronym">CASSIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/cassis</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-866" type="direct"></relation><relation active="#struct-242365" type="indirect"></relation><relation active="#struct-300261" type="indirect"></relation><relation active="#struct-300360" type="indirect"></relation><relation name="UMR6174" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-866" type="direct"><org type="laboratory" xml:id="struct-866" status="VALID"><idno type="IdRef">152639071</idno><idno type="RNSR">200412232H</idno><orgName>Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies</orgName><orgName type="acronym">FEMTO-ST</orgName><desc><address><addrLine>32 avenue de l'Observatoire 25044 BESANCON CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.femto-st.fr</ref></desc><listRelation><relation active="#struct-242365" type="direct"></relation><relation active="#struct-300261" type="direct"></relation><relation active="#struct-300360" type="direct"></relation><relation name="UMR6174" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-242365" type="indirect"><org type="institution" xml:id="struct-242365" status="VALID"><idno type="IdRef">026403188</idno><idno type="ISNI">0000 0001 2188 3779 </idno><orgName>Université de Franche-Comté</orgName><orgName type="acronym">UFC</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.univ-fcomte.fr</ref></desc></org></tutelle><tutelle active="#struct-300261" type="indirect"><org type="institution" xml:id="struct-300261" status="VALID"><orgName>Université de Technologie de Belfort-Montbeliard</orgName><orgName type="acronym">UTBM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300360" type="indirect"><org type="institution" xml:id="struct-300360" status="VALID"><orgName>Ecole Nationale Supérieure de Mécanique et des Microtechniques</orgName><orgName type="acronym">ENSMM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6174" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName><placeName><settlement type="city" wicri:auto="siege">Besançon</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de Franche-Comté</orgName><orgName type="institution" wicri:auto="newGroup">Université de Bourgogne Franche-Comté</orgName><placeName><settlement type="city" wicri:auto="siege">Belfort</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de technologie de Belfort-Montbéliard</orgName></affiliation></author><author><name sortKey="Barletta, Michele" sort="Barletta, Michele" uniqKey="Barletta M" first="Michele" last="Barletta">Michele Barletta</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104762" status="VALID"><orgName>Department of Computer Science / Dipartimento di Informatica [Verona]</orgName><desc><address><addrLine>University of Verona - Strada le Grazie 15 I-37134 Verona Italy</addrLine><country key="IT"></country></address><ref type="url">http://www.di.univr.it/</ref></desc><listRelation><relation active="#struct-306285" type="direct"></relation><relation active="#struct-311240" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-306285" type="direct"><org type="institution" xml:id="struct-306285" status="INCOMING"><orgName>Università degli studi di Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-311240" type="direct"><org type="institution" xml:id="struct-311240" status="INCOMING"><orgName>University of Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Italie</country></affiliation></author><author><name sortKey="Calvi, Alberto" sort="Calvi, Alberto" uniqKey="Calvi A" first="Alberto" last="Calvi">Alberto Calvi</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104762" status="VALID"><orgName>Department of Computer Science / Dipartimento di Informatica [Verona]</orgName><desc><address><addrLine>University of Verona - Strada le Grazie 15 I-37134 Verona Italy</addrLine><country key="IT"></country></address><ref type="url">http://www.di.univr.it/</ref></desc><listRelation><relation active="#struct-306285" type="direct"></relation><relation active="#struct-311240" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-306285" type="direct"><org type="institution" xml:id="struct-306285" status="INCOMING"><orgName>Università degli studi di Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-311240" type="direct"><org type="institution" xml:id="struct-311240" status="INCOMING"><orgName>University of Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Italie</country></affiliation></author><author><name sortKey="Cappai, Alessandro" sort="Cappai, Alessandro" uniqKey="Cappai A" first="Alessandro" last="Cappai">Alessandro Cappai</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-135086" status="VALID"><orgName>Dipartimento di Informatica, Sistemistica e Telematica</orgName><orgName type="acronym">DIST</orgName><desc><address><addrLine>Dipartimento di Informatica, Sistemistica e Telematica Viale F. Causa, 13 16145 GENOVA - ITALIA</addrLine><country key="FR"></country></address><ref type="url">http://www.dist.unige.it/</ref></desc><listRelation><relation active="#struct-301142" type="direct"></relation><relation active="#struct-366388" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-301142" type="direct"><org type="institution" xml:id="struct-301142" status="VALID"><orgName>University of Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-366388" type="direct"><org type="institution" xml:id="struct-366388" status="INCOMING"><orgName>Università di Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Carbone, Roberto" sort="Carbone, Roberto" uniqKey="Carbone R" first="Roberto" last="Carbone">Roberto Carbone</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-135086" status="VALID"><orgName>Dipartimento di Informatica, Sistemistica e Telematica</orgName><orgName type="acronym">DIST</orgName><desc><address><addrLine>Dipartimento di Informatica, Sistemistica e Telematica Viale F. Causa, 13 16145 GENOVA - ITALIA</addrLine><country key="FR"></country></address><ref type="url">http://www.dist.unige.it/</ref></desc><listRelation><relation active="#struct-301142" type="direct"></relation><relation active="#struct-366388" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-301142" type="direct"><org type="institution" xml:id="struct-301142" status="VALID"><orgName>University of Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-366388" type="direct"><org type="institution" xml:id="struct-366388" status="INCOMING"><orgName>Università di Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-34499" status="VALID"><orgName>Institut de recherche en informatique de Toulouse</orgName><orgName type="acronym">IRIT</orgName><desc><address><addrLine>118 Route de Narbonne, F-31062 Toulouse Cedex 9</addrLine><country key="FR"></country></address><ref type="url">http://www.irit.fr/</ref></desc><listRelation><relation active="#struct-5030" type="direct"></relation><relation active="#struct-81148" type="direct"></relation><relation active="#struct-116256" type="direct"></relation><relation active="#struct-217752" type="direct"></relation><relation name="UMR5505" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-5030" type="direct"><org type="institution" xml:id="struct-5030" status="VALID"><orgName>Institut National Polytechnique [Toulouse]</orgName><orgName type="acronym">INP</orgName><desc><address><addrLine>6 allée Émile Monso - BP 34038 - 31029 Toulouse cedex 4</addrLine><country key="FR"></country></address><ref type="url">http://www.inp-toulouse.fr/</ref></desc></org></tutelle><tutelle active="#struct-81148" type="direct"><org type="institution" xml:id="struct-81148" status="VALID"><orgName>Université Toulouse 1 Capitole</orgName><orgName type="acronym">UT1</orgName><desc><address><addrLine>2 rue du Doyen-Gabriel-Marty - 31042 Toulouse Cedex 9 </addrLine><country key="FR"></country></address><ref type="url">http://www.ut-capitole.fr/</ref></desc></org></tutelle><tutelle active="#struct-116256" type="direct"><org type="institution" xml:id="struct-116256" status="VALID"><idno type="IdRef">026403994</idno><orgName>Université Toulouse 2</orgName><orgName type="acronym">UT2</orgName><date type="start">1971-01-01</date><desc><address><addrLine>5 allées Antonio Machado - 31058 Toulouse Cedex 9 </addrLine><country key="FR"></country></address><ref type="url">http://www.univ-tlse2.fr</ref></desc></org></tutelle><tutelle active="#struct-217752" type="direct"><org type="institution" xml:id="struct-217752" status="VALID"><orgName>Université Paul Sabatier - Toulouse 3</orgName><orgName type="acronym">UPS</orgName><desc><address><addrLine>118 route de Narbonne - 31062 Toulouse</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-tlse3.fr/</ref></desc></org></tutelle><tutelle name="UMR5505" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Compagna, Luca" sort="Compagna, Luca" uniqKey="Compagna L" first="Luca" last="Compagna">Luca Compagna</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-132970" status="VALID"><orgName>SAP Research [Sophia Antipolis]</orgName><desc><address><addrLine>805 Avenue du Docteur Maurice Donat, BP1216-06254 Mougins, France</addrLine><country key="FR"></country></address></desc><listRelation><relation active="#struct-301537" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-301537" type="direct"><org type="institution" xml:id="struct-301537" status="VALID"><orgName>SAP Research</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Cuellar, Jorge" sort="Cuellar, Jorge" uniqKey="Cuellar J" first="Jorge" last="Cuellar">Jorge Cuellar</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-101434" status="VALID"><orgName>Software and System Architectures</orgName><orgName type="acronym">Siemens AG Corporate Technology</orgName><desc><address><addrLine>Günter-Scharowsky-Str. 1 91050 Erlangen Germany</addrLine><country key="DE"></country></address></desc><listRelation><relation active="#struct-300755" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300755" type="direct"><org type="institution" xml:id="struct-300755" status="VALID"><orgName>Siemens</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Allemagne</country></affiliation></author><author><name sortKey="Erzse, Gabriel" sort="Erzse, Gabriel" uniqKey="Erzse G" first="Gabriel" last="Erzse">Gabriel Erzse</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-101229" status="VALID"><orgName>Politehnica University of Timisoara</orgName><orgName type="acronym">UPT</orgName><desc><address><addrLine>Bv. V. Pârvan, Nr. 2, 300223, Timisoara</addrLine><country key="RO"></country></address></desc><listRelation><relation active="#struct-321186" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-321186" type="direct"><org type="institution" xml:id="struct-321186" status="INCOMING"><orgName>Politehnica University of Timisoara</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Roumanie</country></affiliation></author><author><name sortKey="Frau, Simone" sort="Frau, Simone" uniqKey="Frau S" first="Simone" last="Frau">Simone Frau</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-83910" status="VALID"><orgName>Department of Computer Science</orgName><orgName type="acronym">ETH Zurich</orgName><desc><address><addrLine>Haldeneggsteig 4 / Weinbergstrasse 8092 Zürich</addrLine><country key="CH"></country></address><ref type="url">http://www.inf.ethz.ch/</ref></desc><listRelation><relation active="#struct-364954" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-364954" type="direct"><org type="institution" xml:id="struct-364954" status="INCOMING"><orgName>ETH ZURICH</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Suisse</country><placeName><settlement type="city">Zurich</settlement><region nuts="3" type="region">Canton de Zurich</region></placeName><orgName type="university">École polytechnique fédérale de Zurich</orgName></affiliation></author><author><name sortKey="Minea, Marius" sort="Minea, Marius" uniqKey="Minea M" first="Marius" last="Minea">Marius Minea</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-101229" status="VALID"><orgName>Politehnica University of Timisoara</orgName><orgName type="acronym">UPT</orgName><desc><address><addrLine>Bv. V. Pârvan, Nr. 2, 300223, Timisoara</addrLine><country key="RO"></country></address></desc><listRelation><relation active="#struct-321186" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-321186" type="direct"><org type="institution" xml:id="struct-321186" status="INCOMING"><orgName>Politehnica University of Timisoara</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Roumanie</country></affiliation></author><author><name sortKey="Modersheim, Sebastian" sort="Modersheim, Sebastian" uniqKey="Modersheim S" first="Sebastian" last="Modersheim">Sebastian Modersheim</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-106019" status="VALID"><orgName>IBM Research Laboratory Zurich</orgName><orgName type="acronym">IBM Research Laboratory Zurich</orgName><desc><address><addrLine>IBM Schweiz Vulkanstrasse 106 Postfach 8010 Zürich</addrLine><country key="FR"></country></address><ref type="url">http://www.zurich.ibm.com/</ref></desc><listRelation><relation active="#struct-300665" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300665" type="direct"><org type="institution" xml:id="struct-300665" status="VALID"><orgName>IBM</orgName><desc><address><country key="US"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Von Oheimb, David" sort="Von Oheimb, David" uniqKey="Von Oheimb D" first="David" last="Von Oheimb">David Von Oheimb</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-101434" status="VALID"><orgName>Software and System Architectures</orgName><orgName type="acronym">Siemens AG Corporate Technology</orgName><desc><address><addrLine>Günter-Scharowsky-Str. 1 91050 Erlangen Germany</addrLine><country key="DE"></country></address></desc><listRelation><relation active="#struct-300755" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300755" type="direct"><org type="institution" xml:id="struct-300755" status="VALID"><orgName>Siemens</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Allemagne</country></affiliation></author><author><name sortKey="Pellegrino, Giancarlo" sort="Pellegrino, Giancarlo" uniqKey="Pellegrino G" first="Giancarlo" last="Pellegrino">Giancarlo Pellegrino</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-132970" status="VALID"><orgName>SAP Research [Sophia Antipolis]</orgName><desc><address><addrLine>805 Avenue du Docteur Maurice Donat, BP1216-06254 Mougins, France</addrLine><country key="FR"></country></address></desc><listRelation><relation active="#struct-301537" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-301537" type="direct"><org type="institution" xml:id="struct-301537" status="VALID"><orgName>SAP Research</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Elisa Ponta, Serena" sort="Elisa Ponta, Serena" uniqKey="Elisa Ponta S" first="Serena" last="Elisa Ponta">Serena Elisa Ponta</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-135086" status="VALID"><orgName>Dipartimento di Informatica, Sistemistica e Telematica</orgName><orgName type="acronym">DIST</orgName><desc><address><addrLine>Dipartimento di Informatica, Sistemistica e Telematica Viale F. Causa, 13 16145 GENOVA - ITALIA</addrLine><country key="FR"></country></address><ref type="url">http://www.dist.unige.it/</ref></desc><listRelation><relation active="#struct-301142" type="direct"></relation><relation active="#struct-366388" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-301142" type="direct"><org type="institution" xml:id="struct-301142" status="VALID"><orgName>University of Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-366388" type="direct"><org type="institution" xml:id="struct-366388" status="INCOMING"><orgName>Università di Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Rocchetto, Marco" sort="Rocchetto, Marco" uniqKey="Rocchetto M" first="Marco" last="Rocchetto">Marco Rocchetto</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104762" status="VALID"><orgName>Department of Computer Science / Dipartimento di Informatica [Verona]</orgName><desc><address><addrLine>University of Verona - Strada le Grazie 15 I-37134 Verona Italy</addrLine><country key="IT"></country></address><ref type="url">http://www.di.univr.it/</ref></desc><listRelation><relation active="#struct-306285" type="direct"></relation><relation active="#struct-311240" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-306285" type="direct"><org type="institution" xml:id="struct-306285" status="INCOMING"><orgName>Università degli studi di Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-311240" type="direct"><org type="institution" xml:id="struct-311240" status="INCOMING"><orgName>University of Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Italie</country></affiliation></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-189789" status="VALID"><idno type="RNSR">200318302K</idno><orgName>Combination of approaches to the security of infinite states systems</orgName><orgName type="acronym">CASSIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/cassis</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-866" type="direct"></relation><relation active="#struct-242365" type="indirect"></relation><relation active="#struct-300261" type="indirect"></relation><relation active="#struct-300360" type="indirect"></relation><relation name="UMR6174" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-866" type="direct"><org type="laboratory" xml:id="struct-866" status="VALID"><idno type="IdRef">152639071</idno><idno type="RNSR">200412232H</idno><orgName>Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies</orgName><orgName type="acronym">FEMTO-ST</orgName><desc><address><addrLine>32 avenue de l'Observatoire 25044 BESANCON CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.femto-st.fr</ref></desc><listRelation><relation active="#struct-242365" type="direct"></relation><relation active="#struct-300261" type="direct"></relation><relation active="#struct-300360" type="direct"></relation><relation name="UMR6174" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-242365" type="indirect"><org type="institution" xml:id="struct-242365" status="VALID"><idno type="IdRef">026403188</idno><idno type="ISNI">0000 0001 2188 3779 </idno><orgName>Université de Franche-Comté</orgName><orgName type="acronym">UFC</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.univ-fcomte.fr</ref></desc></org></tutelle><tutelle active="#struct-300261" type="indirect"><org type="institution" xml:id="struct-300261" status="VALID"><orgName>Université de Technologie de Belfort-Montbeliard</orgName><orgName type="acronym">UTBM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300360" type="indirect"><org type="institution" xml:id="struct-300360" status="VALID"><orgName>Ecole Nationale Supérieure de Mécanique et des Microtechniques</orgName><orgName type="acronym">ENSMM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6174" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName><placeName><settlement type="city" wicri:auto="siege">Besançon</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de Franche-Comté</orgName><orgName type="institution" wicri:auto="newGroup">Université de Bourgogne Franche-Comté</orgName><placeName><settlement type="city" wicri:auto="siege">Belfort</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de technologie de Belfort-Montbéliard</orgName></affiliation></author><author><name sortKey="Torabi Dashti, Mohammad" sort="Torabi Dashti, Mohammad" uniqKey="Torabi Dashti M" first="Mohammad" last="Torabi Dashti">Mohammad Torabi Dashti</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-83910" status="VALID"><orgName>Department of Computer Science</orgName><orgName type="acronym">ETH Zurich</orgName><desc><address><addrLine>Haldeneggsteig 4 / Weinbergstrasse 8092 Zürich</addrLine><country key="CH"></country></address><ref type="url">http://www.inf.ethz.ch/</ref></desc><listRelation><relation active="#struct-364954" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-364954" type="direct"><org type="institution" xml:id="struct-364954" status="INCOMING"><orgName>ETH ZURICH</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Suisse</country><placeName><settlement type="city">Zurich</settlement><region nuts="3" type="region">Canton de Zurich</region></placeName><orgName type="university">École polytechnique fédérale de Zurich</orgName></affiliation></author><author><name sortKey="Turuani, Mathieu" sort="Turuani, Mathieu" uniqKey="Turuani M" first="Mathieu" last="Turuani">Mathieu Turuani</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-189789" status="VALID"><idno type="RNSR">200318302K</idno><orgName>Combination of approaches to the security of infinite states systems</orgName><orgName type="acronym">CASSIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/cassis</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-866" type="direct"></relation><relation active="#struct-242365" type="indirect"></relation><relation active="#struct-300261" type="indirect"></relation><relation active="#struct-300360" type="indirect"></relation><relation name="UMR6174" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-866" type="direct"><org type="laboratory" xml:id="struct-866" status="VALID"><idno type="IdRef">152639071</idno><idno type="RNSR">200412232H</idno><orgName>Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies</orgName><orgName type="acronym">FEMTO-ST</orgName><desc><address><addrLine>32 avenue de l'Observatoire 25044 BESANCON CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.femto-st.fr</ref></desc><listRelation><relation active="#struct-242365" type="direct"></relation><relation active="#struct-300261" type="direct"></relation><relation active="#struct-300360" type="direct"></relation><relation name="UMR6174" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-242365" type="indirect"><org type="institution" xml:id="struct-242365" status="VALID"><idno type="IdRef">026403188</idno><idno type="ISNI">0000 0001 2188 3779 </idno><orgName>Université de Franche-Comté</orgName><orgName type="acronym">UFC</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.univ-fcomte.fr</ref></desc></org></tutelle><tutelle active="#struct-300261" type="indirect"><org type="institution" xml:id="struct-300261" status="VALID"><orgName>Université de Technologie de Belfort-Montbeliard</orgName><orgName type="acronym">UTBM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300360" type="indirect"><org type="institution" xml:id="struct-300360" status="VALID"><orgName>Ecole Nationale Supérieure de Mécanique et des Microtechniques</orgName><orgName type="acronym">ENSMM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6174" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName><placeName><settlement type="city" wicri:auto="siege">Besançon</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de Franche-Comté</orgName><orgName type="institution" wicri:auto="newGroup">Université de Bourgogne Franche-Comté</orgName><placeName><settlement type="city" wicri:auto="siege">Belfort</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de technologie de Belfort-Montbéliard</orgName></affiliation></author><author><name sortKey="Vigano, Luca" sort="Vigano, Luca" uniqKey="Vigano L" first="Luca" last="Vigano">Luca Vigano</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104762" status="VALID"><orgName>Department of Computer Science / Dipartimento di Informatica [Verona]</orgName><desc><address><addrLine>University of Verona - Strada le Grazie 15 I-37134 Verona Italy</addrLine><country key="IT"></country></address><ref type="url">http://www.di.univr.it/</ref></desc><listRelation><relation active="#struct-306285" type="direct"></relation><relation active="#struct-311240" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-306285" type="direct"><org type="institution" xml:id="struct-306285" status="INCOMING"><orgName>Università degli studi di Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-311240" type="direct"><org type="institution" xml:id="struct-311240" status="INCOMING"><orgName>University of Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Italie</country></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:hal-00759725</idno><idno type="halId">hal-00759725</idno><idno type="halUri">https://hal.inria.fr/hal-00759725</idno><idno type="url">https://hal.inria.fr/hal-00759725</idno><idno type="doi">10.1007/978-3-642-28756-5_19</idno><date when="2012-03-24">2012-03-24</date><idno type="wicri:Area/Hal/Corpus">004A90</idno><idno type="wicri:Area/Hal/Curation">004A90</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures</title><author><name sortKey="Armando, Alessandro" sort="Armando, Alessandro" uniqKey="Armando A" first="Alessandro" last="Armando">Alessandro Armando</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-135086" status="VALID"><orgName>Dipartimento di Informatica, Sistemistica e Telematica</orgName><orgName type="acronym">DIST</orgName><desc><address><addrLine>Dipartimento di Informatica, Sistemistica e Telematica Viale F. Causa, 13 16145 GENOVA - ITALIA</addrLine><country key="FR"></country></address><ref type="url">http://www.dist.unige.it/</ref></desc><listRelation><relation active="#struct-301142" type="direct"></relation><relation active="#struct-366388" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-301142" type="direct"><org type="institution" xml:id="struct-301142" status="VALID"><orgName>University of Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-366388" type="direct"><org type="institution" xml:id="struct-366388" status="INCOMING"><orgName>Università di Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Arsac, Wihem" sort="Arsac, Wihem" uniqKey="Arsac W" first="Wihem" last="Arsac">Wihem Arsac</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-132970" status="VALID"><orgName>SAP Research [Sophia Antipolis]</orgName><desc><address><addrLine>805 Avenue du Docteur Maurice Donat, BP1216-06254 Mougins, France</addrLine><country key="FR"></country></address></desc><listRelation><relation active="#struct-301537" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-301537" type="direct"><org type="institution" xml:id="struct-301537" status="VALID"><orgName>SAP Research</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Avanesov, Tigran" sort="Avanesov, Tigran" uniqKey="Avanesov T" first="Tigran" last="Avanesov">Tigran Avanesov</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-189789" status="VALID"><idno type="RNSR">200318302K</idno><orgName>Combination of approaches to the security of infinite states systems</orgName><orgName type="acronym">CASSIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/cassis</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-866" type="direct"></relation><relation active="#struct-242365" type="indirect"></relation><relation active="#struct-300261" type="indirect"></relation><relation active="#struct-300360" type="indirect"></relation><relation name="UMR6174" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-866" type="direct"><org type="laboratory" xml:id="struct-866" status="VALID"><idno type="IdRef">152639071</idno><idno type="RNSR">200412232H</idno><orgName>Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies</orgName><orgName type="acronym">FEMTO-ST</orgName><desc><address><addrLine>32 avenue de l'Observatoire 25044 BESANCON CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.femto-st.fr</ref></desc><listRelation><relation active="#struct-242365" type="direct"></relation><relation active="#struct-300261" type="direct"></relation><relation active="#struct-300360" type="direct"></relation><relation name="UMR6174" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-242365" type="indirect"><org type="institution" xml:id="struct-242365" status="VALID"><idno type="IdRef">026403188</idno><idno type="ISNI">0000 0001 2188 3779 </idno><orgName>Université de Franche-Comté</orgName><orgName type="acronym">UFC</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.univ-fcomte.fr</ref></desc></org></tutelle><tutelle active="#struct-300261" type="indirect"><org type="institution" xml:id="struct-300261" status="VALID"><orgName>Université de Technologie de Belfort-Montbeliard</orgName><orgName type="acronym">UTBM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300360" type="indirect"><org type="institution" xml:id="struct-300360" status="VALID"><orgName>Ecole Nationale Supérieure de Mécanique et des Microtechniques</orgName><orgName type="acronym">ENSMM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6174" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName><placeName><settlement type="city" wicri:auto="siege">Besançon</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de Franche-Comté</orgName><orgName type="institution" wicri:auto="newGroup">Université de Bourgogne Franche-Comté</orgName><placeName><settlement type="city" wicri:auto="siege">Belfort</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de technologie de Belfort-Montbéliard</orgName></affiliation></author><author><name sortKey="Barletta, Michele" sort="Barletta, Michele" uniqKey="Barletta M" first="Michele" last="Barletta">Michele Barletta</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104762" status="VALID"><orgName>Department of Computer Science / Dipartimento di Informatica [Verona]</orgName><desc><address><addrLine>University of Verona - Strada le Grazie 15 I-37134 Verona Italy</addrLine><country key="IT"></country></address><ref type="url">http://www.di.univr.it/</ref></desc><listRelation><relation active="#struct-306285" type="direct"></relation><relation active="#struct-311240" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-306285" type="direct"><org type="institution" xml:id="struct-306285" status="INCOMING"><orgName>Università degli studi di Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-311240" type="direct"><org type="institution" xml:id="struct-311240" status="INCOMING"><orgName>University of Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Italie</country></affiliation></author><author><name sortKey="Calvi, Alberto" sort="Calvi, Alberto" uniqKey="Calvi A" first="Alberto" last="Calvi">Alberto Calvi</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104762" status="VALID"><orgName>Department of Computer Science / Dipartimento di Informatica [Verona]</orgName><desc><address><addrLine>University of Verona - Strada le Grazie 15 I-37134 Verona Italy</addrLine><country key="IT"></country></address><ref type="url">http://www.di.univr.it/</ref></desc><listRelation><relation active="#struct-306285" type="direct"></relation><relation active="#struct-311240" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-306285" type="direct"><org type="institution" xml:id="struct-306285" status="INCOMING"><orgName>Università degli studi di Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-311240" type="direct"><org type="institution" xml:id="struct-311240" status="INCOMING"><orgName>University of Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Italie</country></affiliation></author><author><name sortKey="Cappai, Alessandro" sort="Cappai, Alessandro" uniqKey="Cappai A" first="Alessandro" last="Cappai">Alessandro Cappai</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-135086" status="VALID"><orgName>Dipartimento di Informatica, Sistemistica e Telematica</orgName><orgName type="acronym">DIST</orgName><desc><address><addrLine>Dipartimento di Informatica, Sistemistica e Telematica Viale F. Causa, 13 16145 GENOVA - ITALIA</addrLine><country key="FR"></country></address><ref type="url">http://www.dist.unige.it/</ref></desc><listRelation><relation active="#struct-301142" type="direct"></relation><relation active="#struct-366388" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-301142" type="direct"><org type="institution" xml:id="struct-301142" status="VALID"><orgName>University of Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-366388" type="direct"><org type="institution" xml:id="struct-366388" status="INCOMING"><orgName>Università di Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Carbone, Roberto" sort="Carbone, Roberto" uniqKey="Carbone R" first="Roberto" last="Carbone">Roberto Carbone</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-135086" status="VALID"><orgName>Dipartimento di Informatica, Sistemistica e Telematica</orgName><orgName type="acronym">DIST</orgName><desc><address><addrLine>Dipartimento di Informatica, Sistemistica e Telematica Viale F. Causa, 13 16145 GENOVA - ITALIA</addrLine><country key="FR"></country></address><ref type="url">http://www.dist.unige.it/</ref></desc><listRelation><relation active="#struct-301142" type="direct"></relation><relation active="#struct-366388" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-301142" type="direct"><org type="institution" xml:id="struct-301142" status="VALID"><orgName>University of Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-366388" type="direct"><org type="institution" xml:id="struct-366388" status="INCOMING"><orgName>Università di Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-34499" status="VALID"><orgName>Institut de recherche en informatique de Toulouse</orgName><orgName type="acronym">IRIT</orgName><desc><address><addrLine>118 Route de Narbonne, F-31062 Toulouse Cedex 9</addrLine><country key="FR"></country></address><ref type="url">http://www.irit.fr/</ref></desc><listRelation><relation active="#struct-5030" type="direct"></relation><relation active="#struct-81148" type="direct"></relation><relation active="#struct-116256" type="direct"></relation><relation active="#struct-217752" type="direct"></relation><relation name="UMR5505" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-5030" type="direct"><org type="institution" xml:id="struct-5030" status="VALID"><orgName>Institut National Polytechnique [Toulouse]</orgName><orgName type="acronym">INP</orgName><desc><address><addrLine>6 allée Émile Monso - BP 34038 - 31029 Toulouse cedex 4</addrLine><country key="FR"></country></address><ref type="url">http://www.inp-toulouse.fr/</ref></desc></org></tutelle><tutelle active="#struct-81148" type="direct"><org type="institution" xml:id="struct-81148" status="VALID"><orgName>Université Toulouse 1 Capitole</orgName><orgName type="acronym">UT1</orgName><desc><address><addrLine>2 rue du Doyen-Gabriel-Marty - 31042 Toulouse Cedex 9 </addrLine><country key="FR"></country></address><ref type="url">http://www.ut-capitole.fr/</ref></desc></org></tutelle><tutelle active="#struct-116256" type="direct"><org type="institution" xml:id="struct-116256" status="VALID"><idno type="IdRef">026403994</idno><orgName>Université Toulouse 2</orgName><orgName type="acronym">UT2</orgName><date type="start">1971-01-01</date><desc><address><addrLine>5 allées Antonio Machado - 31058 Toulouse Cedex 9 </addrLine><country key="FR"></country></address><ref type="url">http://www.univ-tlse2.fr</ref></desc></org></tutelle><tutelle active="#struct-217752" type="direct"><org type="institution" xml:id="struct-217752" status="VALID"><orgName>Université Paul Sabatier - Toulouse 3</orgName><orgName type="acronym">UPS</orgName><desc><address><addrLine>118 route de Narbonne - 31062 Toulouse</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-tlse3.fr/</ref></desc></org></tutelle><tutelle name="UMR5505" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Compagna, Luca" sort="Compagna, Luca" uniqKey="Compagna L" first="Luca" last="Compagna">Luca Compagna</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-132970" status="VALID"><orgName>SAP Research [Sophia Antipolis]</orgName><desc><address><addrLine>805 Avenue du Docteur Maurice Donat, BP1216-06254 Mougins, France</addrLine><country key="FR"></country></address></desc><listRelation><relation active="#struct-301537" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-301537" type="direct"><org type="institution" xml:id="struct-301537" status="VALID"><orgName>SAP Research</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Cuellar, Jorge" sort="Cuellar, Jorge" uniqKey="Cuellar J" first="Jorge" last="Cuellar">Jorge Cuellar</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-101434" status="VALID"><orgName>Software and System Architectures</orgName><orgName type="acronym">Siemens AG Corporate Technology</orgName><desc><address><addrLine>Günter-Scharowsky-Str. 1 91050 Erlangen Germany</addrLine><country key="DE"></country></address></desc><listRelation><relation active="#struct-300755" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300755" type="direct"><org type="institution" xml:id="struct-300755" status="VALID"><orgName>Siemens</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Allemagne</country></affiliation></author><author><name sortKey="Erzse, Gabriel" sort="Erzse, Gabriel" uniqKey="Erzse G" first="Gabriel" last="Erzse">Gabriel Erzse</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-101229" status="VALID"><orgName>Politehnica University of Timisoara</orgName><orgName type="acronym">UPT</orgName><desc><address><addrLine>Bv. V. Pârvan, Nr. 2, 300223, Timisoara</addrLine><country key="RO"></country></address></desc><listRelation><relation active="#struct-321186" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-321186" type="direct"><org type="institution" xml:id="struct-321186" status="INCOMING"><orgName>Politehnica University of Timisoara</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Roumanie</country></affiliation></author><author><name sortKey="Frau, Simone" sort="Frau, Simone" uniqKey="Frau S" first="Simone" last="Frau">Simone Frau</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-83910" status="VALID"><orgName>Department of Computer Science</orgName><orgName type="acronym">ETH Zurich</orgName><desc><address><addrLine>Haldeneggsteig 4 / Weinbergstrasse 8092 Zürich</addrLine><country key="CH"></country></address><ref type="url">http://www.inf.ethz.ch/</ref></desc><listRelation><relation active="#struct-364954" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-364954" type="direct"><org type="institution" xml:id="struct-364954" status="INCOMING"><orgName>ETH ZURICH</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Suisse</country><placeName><settlement type="city">Zurich</settlement><region nuts="3" type="region">Canton de Zurich</region></placeName><orgName type="university">École polytechnique fédérale de Zurich</orgName></affiliation></author><author><name sortKey="Minea, Marius" sort="Minea, Marius" uniqKey="Minea M" first="Marius" last="Minea">Marius Minea</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-101229" status="VALID"><orgName>Politehnica University of Timisoara</orgName><orgName type="acronym">UPT</orgName><desc><address><addrLine>Bv. V. Pârvan, Nr. 2, 300223, Timisoara</addrLine><country key="RO"></country></address></desc><listRelation><relation active="#struct-321186" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-321186" type="direct"><org type="institution" xml:id="struct-321186" status="INCOMING"><orgName>Politehnica University of Timisoara</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Roumanie</country></affiliation></author><author><name sortKey="Modersheim, Sebastian" sort="Modersheim, Sebastian" uniqKey="Modersheim S" first="Sebastian" last="Modersheim">Sebastian Modersheim</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-106019" status="VALID"><orgName>IBM Research Laboratory Zurich</orgName><orgName type="acronym">IBM Research Laboratory Zurich</orgName><desc><address><addrLine>IBM Schweiz Vulkanstrasse 106 Postfach 8010 Zürich</addrLine><country key="FR"></country></address><ref type="url">http://www.zurich.ibm.com/</ref></desc><listRelation><relation active="#struct-300665" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300665" type="direct"><org type="institution" xml:id="struct-300665" status="VALID"><orgName>IBM</orgName><desc><address><country key="US"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Von Oheimb, David" sort="Von Oheimb, David" uniqKey="Von Oheimb D" first="David" last="Von Oheimb">David Von Oheimb</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-101434" status="VALID"><orgName>Software and System Architectures</orgName><orgName type="acronym">Siemens AG Corporate Technology</orgName><desc><address><addrLine>Günter-Scharowsky-Str. 1 91050 Erlangen Germany</addrLine><country key="DE"></country></address></desc><listRelation><relation active="#struct-300755" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300755" type="direct"><org type="institution" xml:id="struct-300755" status="VALID"><orgName>Siemens</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Allemagne</country></affiliation></author><author><name sortKey="Pellegrino, Giancarlo" sort="Pellegrino, Giancarlo" uniqKey="Pellegrino G" first="Giancarlo" last="Pellegrino">Giancarlo Pellegrino</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-132970" status="VALID"><orgName>SAP Research [Sophia Antipolis]</orgName><desc><address><addrLine>805 Avenue du Docteur Maurice Donat, BP1216-06254 Mougins, France</addrLine><country key="FR"></country></address></desc><listRelation><relation active="#struct-301537" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-301537" type="direct"><org type="institution" xml:id="struct-301537" status="VALID"><orgName>SAP Research</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Elisa Ponta, Serena" sort="Elisa Ponta, Serena" uniqKey="Elisa Ponta S" first="Serena" last="Elisa Ponta">Serena Elisa Ponta</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-135086" status="VALID"><orgName>Dipartimento di Informatica, Sistemistica e Telematica</orgName><orgName type="acronym">DIST</orgName><desc><address><addrLine>Dipartimento di Informatica, Sistemistica e Telematica Viale F. Causa, 13 16145 GENOVA - ITALIA</addrLine><country key="FR"></country></address><ref type="url">http://www.dist.unige.it/</ref></desc><listRelation><relation active="#struct-301142" type="direct"></relation><relation active="#struct-366388" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-301142" type="direct"><org type="institution" xml:id="struct-301142" status="VALID"><orgName>University of Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-366388" type="direct"><org type="institution" xml:id="struct-366388" status="INCOMING"><orgName>Università di Genova</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Rocchetto, Marco" sort="Rocchetto, Marco" uniqKey="Rocchetto M" first="Marco" last="Rocchetto">Marco Rocchetto</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104762" status="VALID"><orgName>Department of Computer Science / Dipartimento di Informatica [Verona]</orgName><desc><address><addrLine>University of Verona - Strada le Grazie 15 I-37134 Verona Italy</addrLine><country key="IT"></country></address><ref type="url">http://www.di.univr.it/</ref></desc><listRelation><relation active="#struct-306285" type="direct"></relation><relation active="#struct-311240" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-306285" type="direct"><org type="institution" xml:id="struct-306285" status="INCOMING"><orgName>Università degli studi di Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-311240" type="direct"><org type="institution" xml:id="struct-311240" status="INCOMING"><orgName>University of Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Italie</country></affiliation></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-189789" status="VALID"><idno type="RNSR">200318302K</idno><orgName>Combination of approaches to the security of infinite states systems</orgName><orgName type="acronym">CASSIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/cassis</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-866" type="direct"></relation><relation active="#struct-242365" type="indirect"></relation><relation active="#struct-300261" type="indirect"></relation><relation active="#struct-300360" type="indirect"></relation><relation name="UMR6174" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-866" type="direct"><org type="laboratory" xml:id="struct-866" status="VALID"><idno type="IdRef">152639071</idno><idno type="RNSR">200412232H</idno><orgName>Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies</orgName><orgName type="acronym">FEMTO-ST</orgName><desc><address><addrLine>32 avenue de l'Observatoire 25044 BESANCON CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.femto-st.fr</ref></desc><listRelation><relation active="#struct-242365" type="direct"></relation><relation active="#struct-300261" type="direct"></relation><relation active="#struct-300360" type="direct"></relation><relation name="UMR6174" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-242365" type="indirect"><org type="institution" xml:id="struct-242365" status="VALID"><idno type="IdRef">026403188</idno><idno type="ISNI">0000 0001 2188 3779 </idno><orgName>Université de Franche-Comté</orgName><orgName type="acronym">UFC</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.univ-fcomte.fr</ref></desc></org></tutelle><tutelle active="#struct-300261" type="indirect"><org type="institution" xml:id="struct-300261" status="VALID"><orgName>Université de Technologie de Belfort-Montbeliard</orgName><orgName type="acronym">UTBM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300360" type="indirect"><org type="institution" xml:id="struct-300360" status="VALID"><orgName>Ecole Nationale Supérieure de Mécanique et des Microtechniques</orgName><orgName type="acronym">ENSMM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6174" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName><placeName><settlement type="city" wicri:auto="siege">Besançon</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de Franche-Comté</orgName><orgName type="institution" wicri:auto="newGroup">Université de Bourgogne Franche-Comté</orgName><placeName><settlement type="city" wicri:auto="siege">Belfort</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de technologie de Belfort-Montbéliard</orgName></affiliation></author><author><name sortKey="Torabi Dashti, Mohammad" sort="Torabi Dashti, Mohammad" uniqKey="Torabi Dashti M" first="Mohammad" last="Torabi Dashti">Mohammad Torabi Dashti</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-83910" status="VALID"><orgName>Department of Computer Science</orgName><orgName type="acronym">ETH Zurich</orgName><desc><address><addrLine>Haldeneggsteig 4 / Weinbergstrasse 8092 Zürich</addrLine><country key="CH"></country></address><ref type="url">http://www.inf.ethz.ch/</ref></desc><listRelation><relation active="#struct-364954" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-364954" type="direct"><org type="institution" xml:id="struct-364954" status="INCOMING"><orgName>ETH ZURICH</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Suisse</country><placeName><settlement type="city">Zurich</settlement><region nuts="3" type="region">Canton de Zurich</region></placeName><orgName type="university">École polytechnique fédérale de Zurich</orgName></affiliation></author><author><name sortKey="Turuani, Mathieu" sort="Turuani, Mathieu" uniqKey="Turuani M" first="Mathieu" last="Turuani">Mathieu Turuani</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-189789" status="VALID"><idno type="RNSR">200318302K</idno><orgName>Combination of approaches to the security of infinite states systems</orgName><orgName type="acronym">CASSIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/cassis</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-866" type="direct"></relation><relation active="#struct-242365" type="indirect"></relation><relation active="#struct-300261" type="indirect"></relation><relation active="#struct-300360" type="indirect"></relation><relation name="UMR6174" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-866" type="direct"><org type="laboratory" xml:id="struct-866" status="VALID"><idno type="IdRef">152639071</idno><idno type="RNSR">200412232H</idno><orgName>Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies</orgName><orgName type="acronym">FEMTO-ST</orgName><desc><address><addrLine>32 avenue de l'Observatoire 25044 BESANCON CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.femto-st.fr</ref></desc><listRelation><relation active="#struct-242365" type="direct"></relation><relation active="#struct-300261" type="direct"></relation><relation active="#struct-300360" type="direct"></relation><relation name="UMR6174" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-242365" type="indirect"><org type="institution" xml:id="struct-242365" status="VALID"><idno type="IdRef">026403188</idno><idno type="ISNI">0000 0001 2188 3779 </idno><orgName>Université de Franche-Comté</orgName><orgName type="acronym">UFC</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.univ-fcomte.fr</ref></desc></org></tutelle><tutelle active="#struct-300261" type="indirect"><org type="institution" xml:id="struct-300261" status="VALID"><orgName>Université de Technologie de Belfort-Montbeliard</orgName><orgName type="acronym">UTBM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300360" type="indirect"><org type="institution" xml:id="struct-300360" status="VALID"><orgName>Ecole Nationale Supérieure de Mécanique et des Microtechniques</orgName><orgName type="acronym">ENSMM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6174" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName><placeName><settlement type="city" wicri:auto="siege">Besançon</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de Franche-Comté</orgName><orgName type="institution" wicri:auto="newGroup">Université de Bourgogne Franche-Comté</orgName><placeName><settlement type="city" wicri:auto="siege">Belfort</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de technologie de Belfort-Montbéliard</orgName></affiliation></author><author><name sortKey="Vigano, Luca" sort="Vigano, Luca" uniqKey="Vigano L" first="Luca" last="Vigano">Luca Vigano</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-104762" status="VALID"><orgName>Department of Computer Science / Dipartimento di Informatica [Verona]</orgName><desc><address><addrLine>University of Verona - Strada le Grazie 15 I-37134 Verona Italy</addrLine><country key="IT"></country></address><ref type="url">http://www.di.univr.it/</ref></desc><listRelation><relation active="#struct-306285" type="direct"></relation><relation active="#struct-311240" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-306285" type="direct"><org type="institution" xml:id="struct-306285" status="INCOMING"><orgName>Università degli studi di Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-311240" type="direct"><org type="institution" xml:id="struct-311240" status="INCOMING"><orgName>University of Verona</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>Italie</country></affiliation></author></analytic><idno type="DOI">10.1007/978-3-642-28756-5_19</idno></biblStruct></sourceDesc></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">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.</div></front></TEI><hal api="V3"><titleStmt><title xml:lang="en">The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures</title><author role="aut"><persName><forename type="first">Alessandro</forename><surname>Armando</surname></persName><email></email><idno type="halauthor">61786</idno><affiliation ref="#struct-135086"></affiliation></author><author role="aut"><persName><forename type="first">Wihem</forename><surname>Arsac</surname></persName><email></email><idno type="halauthor">790777</idno><affiliation ref="#struct-132970"></affiliation></author><author role="aut"><persName><forename type="first">Tigran</forename><surname>Avanesov</surname></persName><email></email><idno type="halauthor">790778</idno><affiliation ref="#struct-189789"></affiliation></author><author role="aut"><persName><forename type="first">Michele</forename><surname>Barletta</surname></persName><email></email><idno type="halauthor">790779</idno><affiliation ref="#struct-104762"></affiliation></author><author role="aut"><persName><forename type="first">Alberto</forename><surname>Calvi</surname></persName><email></email><idno type="halauthor">790780</idno><affiliation ref="#struct-104762"></affiliation></author><author role="aut"><persName><forename type="first">Alessandro</forename><surname>Cappai</surname></persName><email></email><idno type="halauthor">790781</idno><affiliation ref="#struct-135086"></affiliation></author><author role="aut"><persName><forename type="first">Roberto</forename><surname>Carbone</surname></persName><email></email><idno type="halauthor">790782</idno><affiliation ref="#struct-135086"></affiliation></author><author role="aut"><persName><forename type="first">Yannick</forename><surname>Chevalier</surname></persName><email></email><idno type="halauthor">61789</idno><affiliation ref="#struct-34499"></affiliation></author><author role="aut"><persName><forename type="first">Luca</forename><surname>Compagna</surname></persName><email></email><idno type="halauthor">61790</idno><affiliation ref="#struct-132970"></affiliation></author><author role="aut"><persName><forename type="first">Jorge</forename><surname>Cuellar</surname></persName><email></email><idno type="halauthor">61791</idno><affiliation ref="#struct-101434"></affiliation></author><author role="aut"><persName><forename type="first">Gabriel</forename><surname>Erzse</surname></persName><email></email><idno type="halauthor">790783</idno><affiliation ref="#struct-101229"></affiliation></author><author role="aut"><persName><forename type="first">Simone</forename><surname>Frau</surname></persName><email></email><idno type="halauthor">790784</idno><affiliation ref="#struct-83910"></affiliation></author><author role="aut"><persName><forename type="first">Marius</forename><surname>Minea</surname></persName><email></email><idno type="halauthor">121088</idno><affiliation ref="#struct-101229"></affiliation></author><author role="aut"><persName><forename type="first">Sebastian</forename><surname>Modersheim</surname></persName><email></email><idno type="halauthor">790785</idno><affiliation ref="#struct-106019"></affiliation></author><author role="aut"><persName><forename type="first">David</forename><surname>Von Oheimb</surname></persName><email></email><idno type="halauthor">61797</idno><affiliation ref="#struct-101434"></affiliation></author><author role="aut"><persName><forename type="first">Giancarlo</forename><surname>Pellegrino</surname></persName><email></email><idno type="halauthor">790786</idno><affiliation ref="#struct-132970"></affiliation></author><author role="aut"><persName><forename type="first">Serena</forename><surname>Elisa Ponta</surname></persName><email></email><idno type="halauthor">790787</idno><affiliation ref="#struct-135086"></affiliation><affiliation ref="#struct-132970"></affiliation></author><author role="aut"><persName><forename type="first">Marco</forename><surname>Rocchetto</surname></persName><email></email><idno type="halauthor">790788</idno><affiliation ref="#struct-104762"></affiliation></author><author role="aut"><persName><forename type="first">Michaël</forename><surname>Rusinowitch</surname></persName><email></email><idno type="idhal">michael-rusinowitch</idno><idno type="halauthor">61798</idno><affiliation ref="#struct-189789"></affiliation></author><author role="aut"><persName><forename type="first">Mohammad</forename><surname>Torabi Dashti</surname></persName><email></email><idno type="halauthor">790789</idno><affiliation ref="#struct-83910"></affiliation></author><author role="aut"><persName><forename type="first">Mathieu</forename><surname>Turuani</surname></persName><email></email><idno type="halauthor">61801</idno><affiliation ref="#struct-189789"></affiliation></author><author role="aut"><persName><forename type="first">Luca</forename><surname>Vigano</surname></persName><email></email><idno type="halauthor">61800</idno><affiliation ref="#struct-104762"></affiliation></author><editor role="depositor"><persName><forename>Michaël</forename><surname>Rusinowitch</surname></persName><email>rusi@loria.fr</email></editor><funder ref="#projeurop-18581"></funder></titleStmt><editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2012-12-02 15:30:24</date><date type="whenModified">2015-09-22 01:13:09</date><date type="whenReleased">2012-12-02 15:30:24</date><date type="whenProduced">2012-03-24</date></edition><respStmt><resp>contributor</resp><name key="103876"><persName><forename>Michaël</forename><surname>Rusinowitch</surname></persName><email>rusi@loria.fr</email></name></respStmt></editionStmt><publicationStmt><distributor>CCSD</distributor><idno type="halId">hal-00759725</idno><idno type="halUri">https://hal.inria.fr/hal-00759725</idno><idno type="halBibtex">armando:hal-00759725</idno><idno type="halRefHtml">Cormac Flanagan and Barbara Konig. Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Mar 2012, Tallinn, Estonia. Springer, 7214, pp.267-282, 2012, Lecture Notes in Computer Science. <10.1007/978-3-642-28756-5_19></idno><idno type="halRef">Cormac Flanagan and Barbara Konig. Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Mar 2012, Tallinn, Estonia. Springer, 7214, pp.267-282, 2012, Lecture Notes in Computer Science. <10.1007/978-3-642-28756-5_19></idno></publicationStmt><seriesStmt><idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno><idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno><idno type="stamp" n="UNIV-FCOMTE">Université de Franche-Comté</idno><idno type="stamp" n="INRIA-LORRAINE">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LORIA2">Publications du LORIA</idno><idno type="stamp" n="INRIA-NANCY-GRAND-EST">INRIA Nancy - Grand Est</idno><idno type="stamp" n="LORIA-FM" p="LORIA">Méthodes formelles</idno><idno type="stamp" n="LORIA">LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno><idno type="stamp" n="OPENAIRE">OpenAIRE</idno><idno type="stamp" n="UNIV-TLSE2">Université Toulouse 2</idno><idno type="stamp" n="UNIV-TLSE3">Université Paul Sabatier - Toulouse III</idno><idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno><idno type="stamp" n="UNIV-BM">Université de Technologie de Belfort-Montbeliard</idno><idno type="stamp" n="ENSMM">Ecole Nationale Supérieure de Mécanique et des Microtechniques</idno><idno type="stamp" n="FEMTO-ST" p="UNIV-FCOMTE">Franche-Comté Electronique, Mécanique, Thermique et Optique - Sciences et Technologies</idno><idno type="stamp" n="UNIV-BM-THESE">Université de Technologie de Belfort-Montbeliard</idno><idno type="stamp" n="INPT">Institut National Polytechnique de Toulouse</idno><idno type="stamp" n="INRIA_TEST">INRIA - Institut National de Recherche en Informatique et en Automatique</idno></seriesStmt><notesStmt><note type="audience" n="2">International</note><note type="invited" n="0">No</note><note type="popular" n="0">No</note><note type="peer" n="1">Yes</note><note type="proceedings" n="1">Yes</note></notesStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures</title><author role="aut"><persName><forename type="first">Alessandro</forename><surname>Armando</surname></persName><idno type="halAuthorId">61786</idno><affiliation ref="#struct-135086"></affiliation></author><author role="aut"><persName><forename type="first">Wihem</forename><surname>Arsac</surname></persName><idno type="halAuthorId">790777</idno><affiliation ref="#struct-132970"></affiliation></author><author role="aut"><persName><forename type="first">Tigran</forename><surname>Avanesov</surname></persName><idno type="halAuthorId">790778</idno><affiliation ref="#struct-189789"></affiliation></author><author role="aut"><persName><forename type="first">Michele</forename><surname>Barletta</surname></persName><idno type="halAuthorId">790779</idno><affiliation ref="#struct-104762"></affiliation></author><author role="aut"><persName><forename type="first">Alberto</forename><surname>Calvi</surname></persName><idno type="halAuthorId">790780</idno><affiliation ref="#struct-104762"></affiliation></author><author role="aut"><persName><forename type="first">Alessandro</forename><surname>Cappai</surname></persName><idno type="halAuthorId">790781</idno><affiliation ref="#struct-135086"></affiliation></author><author role="aut"><persName><forename type="first">Roberto</forename><surname>Carbone</surname></persName><idno type="halAuthorId">790782</idno><affiliation ref="#struct-135086"></affiliation></author><author role="aut"><persName><forename type="first">Yannick</forename><surname>Chevalier</surname></persName><idno type="halAuthorId">61789</idno><affiliation ref="#struct-34499"></affiliation></author><author role="aut"><persName><forename type="first">Luca</forename><surname>Compagna</surname></persName><idno type="halAuthorId">61790</idno><affiliation ref="#struct-132970"></affiliation></author><author role="aut"><persName><forename type="first">Jorge</forename><surname>Cuellar</surname></persName><idno type="halAuthorId">61791</idno><affiliation ref="#struct-101434"></affiliation></author><author role="aut"><persName><forename type="first">Gabriel</forename><surname>Erzse</surname></persName><idno type="halAuthorId">790783</idno><affiliation ref="#struct-101229"></affiliation></author><author role="aut"><persName><forename type="first">Simone</forename><surname>Frau</surname></persName><idno type="halAuthorId">790784</idno><affiliation ref="#struct-83910"></affiliation></author><author role="aut"><persName><forename type="first">Marius</forename><surname>Minea</surname></persName><idno type="halAuthorId">121088</idno><affiliation ref="#struct-101229"></affiliation></author><author role="aut"><persName><forename type="first">Sebastian</forename><surname>Modersheim</surname></persName><idno type="halAuthorId">790785</idno><affiliation ref="#struct-106019"></affiliation></author><author role="aut"><persName><forename type="first">David</forename><surname>Von Oheimb</surname></persName><idno type="halAuthorId">61797</idno><affiliation ref="#struct-101434"></affiliation></author><author role="aut"><persName><forename type="first">Giancarlo</forename><surname>Pellegrino</surname></persName><idno type="halAuthorId">790786</idno><affiliation ref="#struct-132970"></affiliation></author><author role="aut"><persName><forename type="first">Serena</forename><surname>Elisa Ponta</surname></persName><idno type="halAuthorId">790787</idno><affiliation ref="#struct-135086"></affiliation><affiliation ref="#struct-132970"></affiliation></author><author role="aut"><persName><forename type="first">Marco</forename><surname>Rocchetto</surname></persName><idno type="halAuthorId">790788</idno><affiliation ref="#struct-104762"></affiliation></author><author role="aut"><persName><forename type="first">Michaël</forename><surname>Rusinowitch</surname></persName><idno type="idHal">michael-rusinowitch</idno><idno type="halAuthorId">61798</idno><affiliation ref="#struct-189789"></affiliation></author><author role="aut"><persName><forename type="first">Mohammad</forename><surname>Torabi Dashti</surname></persName><idno type="halAuthorId">790789</idno><affiliation ref="#struct-83910"></affiliation></author><author role="aut"><persName><forename type="first">Mathieu</forename><surname>Turuani</surname></persName><idno type="halAuthorId">61801</idno><affiliation ref="#struct-189789"></affiliation></author><author role="aut"><persName><forename type="first">Luca</forename><surname>Vigano</surname></persName><idno type="halAuthorId">61800</idno><affiliation ref="#struct-104762"></affiliation></author></analytic><monogr><meeting><title>Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012</title><date type="start">2012-03-24</date><date type="end">2012-04-01</date><settlement>Tallinn</settlement><country key="EE">Estonia</country></meeting><editor>Cormac Flanagan and Barbara Konig</editor><imprint><publisher>Springer</publisher><biblScope unit="serie">Lecture Notes in Computer Science</biblScope><biblScope unit="volume">7214</biblScope><biblScope unit="pp">267-282</biblScope><date type="datePub">2012</date></imprint></monogr><idno type="doi">10.1007/978-3-642-28756-5_19</idno></biblStruct></sourceDesc><profileDesc><langUsage><language ident="en">English</language></langUsage><textClass><classCode scheme="halDomain" n="info.info-lo">Computer Science [cs]/Logic in Computer Science [cs.LO]</classCode><classCode scheme="halTypology" n="COMM">Conference papers</classCode></textClass><abstract xml:lang="en">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.</abstract></profileDesc></hal></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004A90 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Hal/Curation/biblio.hfd -nk 004A90 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Hal
|étape= Curation
|type= RBID
|clé= Hal:hal-00759725
|texte= The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures
}}
| This area was generated with Dilib version V0.6.33. |  |