{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T17:30:25Z","timestamp":1648575025509},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T00:00:00Z","timestamp":1309478400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2011,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            CaPiTo allows the modelling of service-oriented applications using process algebras at three levels of abstraction. The\n            <jats:italic>abstract<\/jats:italic>\n            level focuses on the key functionality of the services; the\n            <jats:italic>plug-in<\/jats:italic>\n            level shows how to obtain security using standardised protocol stacks; finally, the\n            <jats:italic>concrete<\/jats:italic>\n            level allows to consider how security is obtained using asymmetric and symmetric cryptographic primitives. The CaPiTo approach therefore caters for a variety of developers that need to cooperate on designing and implementing service-oriented applications. We show how to formally analyse CaPiTo specifications for ensuring the absence of security flaws. The method used is based on static analysis of the corresponding LySa specifications. We illustrate the development on two industrial case studies; one taken from the banking sector and the other a single sign-on protocol.\n          <\/jats:p>","DOI":"10.1007\/s00165-011-0174-7","type":"journal-article","created":{"date-parts":[[2011,3,31]],"date-time":"2011-03-31T07:24:47Z","timestamp":1301556287000},"source":"Crossref","is-referenced-by-count":0,"title":["CaPiTo: protocol stacks for services"],"prefix":"10.1145","volume":"23","author":[{"given":"Han","family":"Gao","sequence":"first","affiliation":[{"name":"DTU Informatics, Technical University of Denmark, Kongens Lyngby, Denmark"}]},{"given":"Flemming","family":"Nielson","sequence":"additional","affiliation":[{"name":"DTU Informatics, Technical University of Denmark, Kongens Lyngby, Denmark"}]},{"given":"Hanne Riis","family":"Nielson","sequence":"additional","affiliation":[{"name":"DTU Informatics, Technical University of Denmark, Kongens Lyngby, Denmark"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Armando A Carbone R Compagna L Cuellar J Abad LT (2008) Formal analysis of SAML 2.0 Web browser single sign-on: breaking the SAML-based single sign-on for Google Apps. In: The 6th ACM workshop on formal methods in security engineering (FMSE 2008). Hilton Alexandria Mark Center Virginia USA. ACM Press","DOI":"10.1145\/1456396.1456397"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2740"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/1145948.1145950"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Boreale M Bruni R Nicola R Loreti M (2008) Sessions and pipelines for structured service programming. In: Proceedings of the 10th IFIP WG 6.1 international conference on formal methods for open object-based distributed systems FMOODS \u201908. Springer Berlin pp 19\u201338","DOI":"10.1007\/978-3-540-68863-1_3"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Dierks T Allen C (1999) The tls protocol version 1.0","DOI":"10.17487\/rfc2246"},{"key":"e_1_2_1_2_6_2","unstructured":"Gao H (2008) Analysis of security protocols by annotations. PhD thesis Technical University of Denmark"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Gao H Nielson F Nielson HR (2011) Analysing protocol stacks for services. In: Rigorous software engineering for service-oriented systems. Springer LNCS (to appear)","DOI":"10.1007\/978-3-642-20401-2_17"},{"key":"e_1_2_1_2_8_2","unstructured":"Hughes J Maler E (2004) Security assertion markup language (SAML) v1.1 technical overview. Technical report"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Hansen SM Skriver J Nielson HR (2005) Using static analysis to validate the saml single sign-on protocol. In: Proceedings of the 2005 workshop on issues in the theory of security WITS \u201905 New York NY USA. ACM pp 27\u201340","DOI":"10.1145\/1045405.1045409"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","first-page":"2000","DOI":"10.1016\/S0140-3664(99)00239-X","article-title":"Verification of security protocols using lotos\u2014method and application","volume":"23","author":"Leduc G","year":"2000","journal-title":"Comput Commun"},{"key":"e_1_2_1_2_11_2","unstructured":"Liberty alliance project. http:\/\/www.projectliberty.org\/"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Lapadula A Pugliese R Tiezzi F (2007) A calculus for orchestration of web services. In: Proceedings of the 16th European conference on programming ESOP\u201907. Springer Berlin pp 33\u201347","DOI":"10.1007\/978-3-540-71316-6_4"},{"key":"e_1_2_1_2_13_2","volume-title":"Communicating and mobile systems: the pgr;-calculus","author":"Milner R","year":"1999"},{"key":"e_1_2_1_2_14_2","first-page":"166","volume-title":"The open-source fixed-point model checker for symbolic analysis of security protocols","author":"M\u00f6dersheim S","year":"2009"},{"key":"e_1_2_1_2_15_2","unstructured":"Nielsen CR Alessandrini M Pollmeier M Nielson HR (2007) Formalising the S&N credit request. Technical report Technical University of Denmark Informatics and Mathematical Modelling Technical University"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Nielson HR Nielson F Pilegaard H (2011) Flow logic for process calculi. ACM Comput Surv (to appear)","DOI":"10.1145\/2071389.2071392"},{"key":"e_1_2_1_2_17_2","first-page":"335","article-title":"A succinct solver for alfp","volume":"9","author":"Nielson F","year":"2002","journal-title":"Nordic J Comput"},{"key":"e_1_2_1_2_18_2","unstructured":"Organization for the advancement of structured information standards. http:\/\/www.oasis-open.org\/home\/index.php"},{"key":"e_1_2_1_2_19_2","unstructured":"O\u2019Shea N. The elyjah project. http:\/\/homepages.inf.ed.ac.uk\/s0237477\/"},{"key":"e_1_2_1_2_20_2","unstructured":"Itu-t x.200 (07\/94) the basic reference model (osi). http:\/\/www.cisco.com\/en\/US\/docs\/internetworking\/technology\/handbook\/OSI-Protocols.html"},{"key":"e_1_2_1_2_21_2","unstructured":"Proverif: Cryptographic protocol verifier in the formal model. http:\/\/www.proverif.ens.fr\/"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.5555\/3405"},{"key":"e_1_2_1_2_23_2","unstructured":"Scyther tool. http:\/\/people.inf.ethz.ch\/cremersc\/scyther\/"},{"key":"e_1_2_1_2_24_2","unstructured":"Sensoria project. http:\/\/sensoria.fast.de\/"},{"key":"e_1_2_1_2_25_2","unstructured":"Shibboleth project. http:\/\/shibboleth.internet2.edu\/index.html"},{"key":"e_1_2_1_2_26_2","unstructured":"Simple object access protocol (soap). http:\/\/www.w3.org\/TR\/#tr_SOAP"},{"key":"e_1_2_1_2_27_2","unstructured":"Stallings W (1999) Cryptography and network security 2nd edn. Principles and practice. Prentice-Hall Upper Saddle River"},{"key":"e_1_2_1_2_28_2","unstructured":"Oasis web services security (wss) tc. http:\/\/www.oasis-open.org\/committees\/tc_home.php?wg_abbrev=wss"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0174-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0174-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0174-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:02:44Z","timestamp":1641484964000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0174-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,7]]}},"alternative-id":["10.1007\/s00165-011-0174-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0174-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,7]]},"article-number":"s00165-011-0174-7"}}