{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,29]],"date-time":"2025-10-29T02:51:27Z","timestamp":1761706287566,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642287558"},{"type":"electronic","value":"9783642287565"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28756-5_19","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:57:15Z","timestamp":1332449835000},"page":"267-282","source":"Crossref","is-referenced-by-count":60,"title":["The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wihem","family":"Arsac","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tigran","family":"Avanesov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michele","family":"Barletta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Calvi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Cappai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Carbone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yannick","family":"Chevalier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Compagna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jorge","family":"Cu\u00e9llar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriel","family":"Erzse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simone","family":"Frau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marius","family":"Minea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"M\u00f6dersheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"von Oheimb","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giancarlo","family":"Pellegrino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Serena Elisa","family":"Ponta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Rocchetto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Rusinowitch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohammad","family":"Torabi Dashti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathieu","family":"Turuani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Vigan\u00f2","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Ritter, E., Ryan, M.D.: StatVerif: Verification of Stateful Processes. In: Proc.\u00a0CSF 2011, pp. 33\u201347. IEEE CS Press (2011)","DOI":"10.1109\/CSF.2011.10"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A. Armando","year":"2005","unstructured":"Armando, A., Basin, D.A., Boichut, Y., Chevalier, Y., Compagna, L., Cu\u00e9llar, J., Drielsma, P.H., H\u00e9am, P.-C., Kouchnarenko, O., Mantovani, J., M\u00f6dersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Vigan\u00f2, L., Vigneron, L.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 281\u2013285. Springer, Heidelberg (2005)"},{"issue":"4","key":"19_CR3","doi-asserted-by":"publisher","first-page":"403","DOI":"10.3166\/jancl.19.403-429","volume":"19","author":"A. Armando","year":"2009","unstructured":"Armando, A., Carbone, R., Compagna, L.: LTL Model Checking for Security Protocols. Journal of Applied Non-Classical Logics\u00a019(4), 403\u2013429 (2009)","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"19_CR4","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-642-21424-0_6","volume-title":"Future Challenges in Security and Privacy for Academia and Industry","author":"A. Armando","year":"2011","unstructured":"Armando, A., Carbone, R., Compagna, L., Cu\u00e9llar, J., Pellegrino, G., Sorniotti, A.: From Multiple Credentials to Browser-Based Single Sign-On: Are We More Secure? In: Camenisch, J., Fischer-H\u00fcbner, S., Murayama, Y., Portmann, A., Rieder, C. (eds.) SEC 2011. IFIP Advances in Information and Communication Technology, vol.\u00a0354, pp. 68\u201379. Springer, Heidelberg (2011)"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Armando, A., Carbone, R., Compagna, L., Cu\u00e9llar, J., Tobarra Abad, L.: Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps. In: Proc.\u00a0FMSE 2008. ACM Press (2008)","DOI":"10.1145\/1456396.1456397"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-02002-5_2","volume-title":"Formal to Practical Security","author":"C. Arora","year":"2009","unstructured":"Arora, C., Turuani, M.: Validating Integrity for the Ephemerizer\u2019s Protocol with CL-Atse. In: Cortier, V., Kirchner, C., Okada, M., Sakurada, H. (eds.) Formal to Practical Security. LNCS, vol.\u00a05458, pp. 21\u201332. Springer, Heidelberg (2009)"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Arsac, W., Compagna, L., Kaluvuri, S., Ponta, S.E.: Security Validation Tool for Business Processes. In: Proc.\u00a0SACMAT 2011, pp. 143\u2013144. ACM (2011)","DOI":"10.1145\/1998441.1998463"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-642-19125-1_3","volume-title":"Engineering Secure Software and Systems","author":"W. Arsac","year":"2011","unstructured":"Arsac, W., Compagna, L., Pellegrino, G., Ponta, S.E.: Security Validation of Business Processes via Model-Checking. In: Erlingsson, \u00da., Wieringa, R., Zannone, N. (eds.) ESSoS 2011. LNCS, vol.\u00a06542, pp. 29\u201342. Springer, Heidelberg (2011)"},{"key":"19_CR9","unstructured":"AVANTSSAR. Deliverable 2.1: Requirements for modelling and ASLan v.1 (2008)"},{"key":"19_CR10","unstructured":"AVANTSSAR. Deliverable 4.2: AVANTSSAR Validation Platform v.2 (2010)"},{"key":"19_CR11","unstructured":"AVANTSSAR. Deliverable 5.4: Assessment of the AVANTSSAR Validation Platform (2010)"},{"key":"19_CR12","unstructured":"AVANTSSAR. Deliverable 6.2.3: Migration to industrial development environments: lessons learned and best practices (2010)"},{"key":"19_CR13","unstructured":"AVANTSSAR. Deliverable 2.3: ASLan++ specification and tutorial (2011)"},{"key":"19_CR14","unstructured":"AVISPA: Automated Validation of Internet Security Protocols and Applications, http:\/\/www.avispa-project.org"},{"issue":"3","key":"19_CR15","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"D. Basin","year":"2005","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: A symbolic model checker for security protocols. IJIS\u00a04(3), 181\u2013208 (2005)","journal-title":"IJIS"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-540-30101-1_9","volume-title":"Formal Methods for Components and Objects","author":"K. Bhargavan","year":"2004","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.D., Pucella, R.: TulaFale: A Security Tool for Web Services. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol.\u00a03188, pp. 197\u2013222. Springer, Heidelberg (2004)"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/11841197_6","volume-title":"Web Services and Formal Methods","author":"K. Bhargavan","year":"2006","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.: Verified Reference Implementations of WS-Security Protocols. In: Bravetti, M., N\u00fa\u00f1ez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol.\u00a04184, pp. 88\u2013106. Springer, Heidelberg (2006)"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Proc.\u00a0CSFW 2001, pp. 82\u201396. IEEE CS Press (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Riis Nielson, H.: Automatic validation of protocol narration. In: Proc.\u00a0CSFW 2003, pp. 126\u2013140. IEEE CS Press (2003)","DOI":"10.1109\/CSFW.2003.1212709"},{"key":"19_CR20","unstructured":"Boichut, Y., Heam, P.-C., Kouchnarenko, O.: TA4SP: Tree Automata based on Automatic Approximations for the Analysis of Security Protocols (2004)"},{"key":"19_CR21","unstructured":"Boichut, Y., Heam, P.-C., Kouchnarenko, O., Oehl, F.: Improvements on the Genet and Klay Technique to Automatically Verify Security Protocols. In: Proc.\u00a0AVIS 2004. ENTCS (2004)"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-12459-4_18","volume-title":"Formal Aspects in Security and Trust","author":"A. Brucker","year":"2010","unstructured":"Brucker, A., M\u00f6dersheim, S.: Integrating Automated and Interactive Protocol Verification. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol.\u00a05983, pp. 248\u2013262. Springer, Heidelberg (2010)"},{"key":"19_CR23","unstructured":"Chevalier, Y., Compagna, L., Cu\u00e9llar, J., Hankes Drielsma, P., Mantovani, J., M\u00f6dersheim, S., Vigneron, L.: A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols. In: Proc.\u00a0SAPS 2004, pp. 193\u2013205 (2004)"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., Mekki, M.A., Rusinowitch, M.: Automatic Composition of Services with Security Policies. In: Proc.\u00a0WSCA, pp. 529\u2013537. IEEE CS Press (2008)","DOI":"10.1109\/SERVICES-1.2008.13"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Comon-Lundh, H., Cortier, V.: New Decidability Results for Fragments of First-order Logic and Application to Cryptographic protocols. TR LSV-03-3, Laboratoire Specification and Verification, ENS de Cachan, France (2003)","DOI":"10.1007\/3-540-44881-0_12"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A.: On the Security of Public-Key Protocols. IEEE Transactions on Information Theory\u00a02(29) (1983)","DOI":"10.1109\/TIT.1983.1056650"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Hodkinson, I., Reynolds, M.: Temporal Logic. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, pp. 655\u2013720. Elsevier (2006)","DOI":"10.1016\/S1570-2464(07)80014-0"},{"issue":"1","key":"19_CR28","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1016\/j.jlap.2006.05.007","volume":"70","author":"R. Lucchi","year":"2007","unstructured":"Lucchi, R., Mazzara, M.: A pi-calculus based semantics for WS-BPEL. J. Log. Algebr. Program.\u00a070(1), 96\u2013118 (2007)","journal-title":"J. Log. Algebr. Program."},{"key":"19_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-01918-0_3","volume-title":"Formal Methods for Web Services","author":"A. Marconi","year":"2009","unstructured":"Marconi, A., Pistore, M.: Synthesis and Composition of Web Services. In: Bernardo, M., Padovani, L., Zavattaro, G. (eds.) SFM 2009. LNCS, vol.\u00a05569, pp. 89\u2013157. Springer, Heidelberg (2009)"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"M\u00f6dersheim, S.: Algebraic Properties in Alice and Bob Notation. In: Proc.\u00a0Ares 2009, pp. 433\u2013440. IEEE CS Press (2009)","DOI":"10.1109\/ARES.2009.95"},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"M\u00f6dersheim, S.: Abstraction by Set-Membership: Verifying Security Protocols and Web Services with Databases. In: Proc.\u00a0CCS 17, pp. 351\u2013360. ACM Press (2010)","DOI":"10.1145\/1866307.1866348"},{"key":"19_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-642-04444-1_21","volume-title":"Computer Security \u2013 ESORICS 2009","author":"S. M\u00f6dersheim","year":"2009","unstructured":"M\u00f6dersheim, S., Vigan\u00f2, L.: Secure Pseudonymous Channels. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol.\u00a05789, pp. 337\u2013354. Springer, Heidelberg (2009)"},{"key":"19_CR33","series-title":"LNCS","first-page":"166","volume-title":"Fosad 2007-2008-2009","author":"S. M\u00f6dersheim","year":"2009","unstructured":"M\u00f6dersheim, S., Vigan\u00f2, L.: The Open-source Fixed-point Model Checker for Symbolic Analysis of Security Protocols. In: Aldini, A., Barth, G., Gorrieri, R. (eds.) FOSAD 2007. LNCS, vol.\u00a05705, pp. 166\u2013194. Springer, Heidelberg (2009)"},{"key":"19_CR34","unstructured":"OASIS. Web Services Business Process Execution Language Version 2.0. (April 11, 2007), http:\/\/docs.asis-open.org\/wsbpel\/2.0\/OS\/wsbpel-v2.0-OS.pdf"},{"key":"19_CR35","unstructured":"OASIS. SAML v2.0 \u2013 Technical Overview (March 2007), http:\/\/www.oasis-open.org\/committees\/tc_home.php?wg_abbrev=security"},{"key":"19_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/11805618_21","volume-title":"Term Rewriting and Applications","author":"M. Turuani","year":"2006","unstructured":"Turuani, M.: The CL-Atse Protocol Analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 277\u2013286. Springer, Heidelberg (2006)"},{"key":"19_CR37","doi-asserted-by":"crossref","unstructured":"von Oheimb, D., M\u00f6dersheim, S.: ASLan++ \u2014 A Formal Security Specification Language for Distributed Systems. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol.\u00a06957, pp. 1\u201322. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-25271-6_1"},{"key":"19_CR38","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"Automated Deduction - CADE-16","author":"C. Weidenbach","year":"1999","unstructured":"Weidenbach, C.: Towards an Automatic Analysis of Security Protocols in First-Order Logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 314\u2013328. Springer, Heidelberg (1999)"},{"key":"19_CR39","unstructured":"WSO2. Web Services Framework for PHP (2006), http:\/\/wso2.org\/projects\/wsf\/php"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28756-5_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T18:53:58Z","timestamp":1742756038000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28756-5_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287558","9783642287565"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28756-5_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}