Online citations, reference lists, and bibliographies.

The AVANTSSAR Platform For The Automated Validation Of Trust And Security Of Service-Oriented Architectures

A. Armando, Wihem Arsac, T. Avanesov, M. Barletta, A. Calvi, Alessandro Cappai, R. Carbone, Y. Chevalier, L. Compagna, J. Cuéllar, G. Erzse, Simone Frau, M. Minea, S. Mödersheim, David von Oheimb, G. Pellegrino, Serena Elisa Ponta, M. Rocchetto, Michaël Rusinowitch, M. T. Dashti, Mathieu Turuani, L. Viganò
Published 2012 · Computer Science

Cite This
Download PDF
Analyze on Scholarcy
Share
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.
This paper references
10.1007/3-540-44881-0_12
New Decidability Results for Fragments of First-Order Logic and Application to Cryptographic Protocols
Hubert Comon-Lundh (2003)
Improvements on the Genet and Klay technique to automatically verify security protocols
Yohan Boichut (2004)
10.1016/J.JLAP.2006.05.007
A pi-calculus based semantics for WS-BPEL
R. Lucchi (2007)
10.1007/978-3-642-21424-0_6
From Multiple Credentials to Browser-Based Single Sign-On: Are We More Secure?
A. Armando (2011)
10.1007/978-3-642-01918-0_3
Synthesis and Composition of Web Services
A. Marconi (2009)
AVISPA: Automated Validation of Internet Security Protocols and Applications. www.avispa-project.org
10.1016/J.COSE.2013.01.003
Future Challenges in Security and Privacy for Academia and Industry
J. Camenisch (2011)
10.1007/978-3-642-01918-0
Formal Methods for Web Services
Marco Bernardo (2009)
TA4SP: Tree Automata based on Automatic Approximations for the Analysis of Security Protocols
Y Boichut (2004)
10.1007/3-540-48660-7_29
Towards an Automatic Analysis of Security Protocols in First-Order Logic
Christoph Weidenbach (1999)
10.1007/978-3-540-30101-1_9
TulaFale: A Security Tool for Web Services
K. Bhargavan (2003)
A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols
Y. Chevalier (2004)
10.1007/978-3-642-03829-7_6
The Open-Source Fixed-Point Model Checker for Symbolic Analysis of Security Protocols
Sebastian Mödersheim (2009)
10.1007/s10207-004-0055-7
OFMC: A symbolic model checker for security protocols
D. Basin (2004)
10.1007/11513988_27
The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications
A. Armando (2005)
Deliverable 5.4: Assessment of the AVANTSSAR Validation Platform
Avantssar (2010)
10.1007/11841197_6
Verified Reference Implementations of WS-Security Protocols
K. Bhargavan (2006)
Web Services Business Process Execution Language Version 2.0 (OASIS Standard)
Sandra Alves (2007)
10.1007/11805618_21
The CL-Atse Protocol Analyser
Mathieu Turuani (2006)
10.1007/978-3-540-75227-1
Formal Aspects in Security and Trust, Fourth International Workshop, FAST 2006, Hamilton, Ontario, Canada, August 26-27, 2006, Revised Selected Papers
T. Dimitrakos (2007)
Deliverable 2.1: Requirements for modelling and ASLan v
Avantssar (2008)
10.1145/1866307.1866348
Abstraction by set-membership: verifying security protocols and web services with databases
S. Mödersheim (2010)
OASIS. SAML v2.0 – Technical Overview. http://www.oasis-open.org/ committees/tc_home.php?wg_abbrev=security
(2007)
Deliverable 4.2: AVANTSSAR Validation Platform v
Avantssar (2010)
10.1007/978-3-642-25271-6_1
ASLan++ - A Formal Security Specification Language for Distributed Systems
David von Oheimb (2010)
10.1016/S1570-2464(07)80014-0
Temporal logic
I. Hodkinson (2007)
10.1007/3-540-48660-7
Automated Deduction — CADE-16
H. Ganzinger (2002)
Web Services Framework for PHP. wso2.org/projects/wsf/php
Wso (2006)
10.1007/978-0-387-39940-9_4015
Web Services Business Process Execution Language
Y. Goland (2009)
10.1007/978-3-642-04444-1_21
Secure Pseudonymous Channels
S. Mödersheim (2009)
10.1007/978-3-642-02002-5_2
Validating Integrity for the Ephemerizer's Protocol with CL-Atse
Charu Arora (2009)
Deliverable 6.2.3: Migration to industrial development environments: lessons learned and best practices
Avantssar (2010)
Migration to industrial development environments: lessons learned and best practices
AVANTSSAR (2010)
10.1109/CSFW.2001.930138
An efficient cryptographic protocol verifier based on prolog rules
B. Blanchet (2001)
10.1109/SERVICES-1.2008.13
Automatic Composition of Services with Security Policies
Y. Chevalier (2008)
10.1007/978-3-642-12459-4_18
Integrating Automated and Interactive Protocol Verification
Achim D. Brucker (2009)
10.1007/978-3-642-19125-1_3
Security Validation of Business Processes via Model-Checking
Wihem Arsac (2011)
10.1145/1456396.1456397
Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for google apps
A. Armando (2008)
10.1109/ARES.2009.95
Algebraic Properties in Alice and Bob Notation
Sebastian Mödersheim (2009)
10.3233/JCS-140501
StatVerif: Verification of Stateful Processes
Myrto Arapinis (2011)
10.1007/3-540-11205-7_4
Temporal Logic
Nicholas Rescher (1971)
Deliverable 2.3: ASLan++ specification and tutorial
Avantssar (2011)
10.1109/CSFW.2003.1212709
Automatic validation of protocol narration
C. Bodei (2003)
10.1007/978-3-642-19125-1
Engineering Secure Software and Systems
Úlfar Erlingsson (2011)
10.1007/BFb0013976
Temporal Logic
P. Øhrstrøm (1994)
10.1109/TIT.1983.1056650
On the security of public key protocols
D. Dolev (1981)
10.1007/978-3-642-04444-1
Computer Security - ESORICS 2009, 14th European Symposium on Research in Computer Security, Saint-Malo, France, September 21-23, 2009. Proceedings
Michael Backes (2009)
10.1007/978-3-540-32033-3_15
Call-by-Value Is Dual to Call-by-Name - Reloaded
P. Wadler (2005)
10.1007/978-3-642-02002-5
Formal to Practical Security - Papers Issued from the 2005-2008 French-Japanese Collaboration
Véronique Cortier (2009)
10.1109/CSF.2007.24
LTL Model Checking for Security Protocols
A. Armando (2007)
10.1145/1998441.1998463
Security validation tool for business processes
Wihem Arsac (2011)



This paper is referenced by
10.3233/JCS-171070
A method for unbounded verification of privacy-type properties
Lucca Hirschi (2019)
10.1109/CSF.2015.20
Set-Pi: Set Membership p-Calculus
A. Bruni (2015)
Security Analysis of the Open Banking Account and Transaction API Protocol
Abdulaziz Almehrej (2020)
10.1016/j.jnca.2013.06.002
KEDGEN2: A key establishment and derivation protocol for EPC Gen2 RFID systems
Wiem Tounsi (2014)
10.1007/978-3-319-49100-4_2
Cross-Tool Semantics for Protocol Security Goals
Joshua D. Guttman (2016)
Network of Excellence Deliverable D9.3 Initial Prototypal Support for Security Assurance for Ser- vices
C. Sprenger (2012)
10.1109/ICSESS.2015.7338996
Abstracting security-critical applications for model checking in a model-driven approach
Marian Borek (2015)
10.1007/978-3-662-54054-1_3
Secure Integration of Third Party Components in a Model-Driven Approach
Marian Borek (2016)
10.23638/LMCS-13(2:8)2017
A Reduced Semantics for Deciding Trace Equivalence
David Baelde (2017)
A CLOUDLET BASED SECURITY AND TRUST MODEL FOR E-GOVERNMENT WEB SERVICES
Bassam Al-Shargabi (2020)
10.1007/978-3-319-25527-9_7
Alice and Bob: Reconciling Formal Models and Implementation
Omar Almousa (2015)
10.1049/iet-sen.2018.5028
State of runtime adaptation in service-oriented systems: what, where, when, how and right
Leah Mutanu (2019)
10.1145/3277570.3277575
A brief look at the security of DeviceNet communication in industrial control systems
Pal-Stefan Murvay (2018)
10.3233/JCS-150536
Service security and privacy as a socio-technical problem
G. Bella (2015)
10.1007/978-3-642-38631-2_63
Formal Modeling and Automatic Security Analysis of Two-Factor and Two-Channel Authentication Protocols
Alessandro Armando (2013)
10.1007/978-3-642-41707-8_19
A Tool for Supporting Developers in Analyzing the Security of Web-Based Security Protocols
G. Pellegrino (2013)
10.1007/978-3-319-09885-2_17
Security and Privacy Concerns About the RFID Layer of EPC Gen2 Networks
Joaquín García (2015)
Composition results for equivalence-based security properties
Stéphanie Delaune (2015)
10.1007/978-3-642-38004-4_7
Analysis of Communicating Authorization Policies
Simone Frau (2012)
Alice and Bob: Reconciling Formal Models and Implementation
Sebastían Alexander (2016)
10.1007/978-3-319-66402-6_12
Modular Verification of Protocol Equivalence in the Presence of Randomness
Matthew S. Bauer (2017)
10.1109/HASE.2015.20
Verification for OAuth Using ASLan++
Haixing Yan (2015)
Security Protocols: Specification, Verification, Implementation, and Composition
Omar Almousa (2016)
Explorer Composing Security Protocols : From Confidentiality to Privacy
Myrto Arapinis (2017)
Analysing Privacy-Type Properties in Cryptographic Protocols
Stéphanie Delaune (2015)
Deciding Security for a Fragment of ASLan (Extended Version)
S. Mödersheim (2012)
10.1007/978-3-319-07452-8_6
On the Synthesis of Secure Services Composition
José Antonio Martín (2014)
10.1007/978-3-319-47846-3_12
CPDY: Extending the Dolev-Yao Attacker with Physical-Layer Interactions
M. Rocchetto (2016)
10.1007/978-3-642-41098-7_7
Using Interpolation for the Verification of Security Protocols
Marco Rocchetto (2013)
10.4018/ijsse.2014010101
Validation of a Trust Approach in Multi-Organization Environments
Khalifa Toumi (2014)
10.1109/ICST.2015.7102630
Security Threat Identification and Testing
Roberto Carbone (2015)
End to end security in service oriented architecture
M. Azarmi (2014)
See more
Semantic Scholar Logo Some data provided by SemanticScholar