{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T16:35:36Z","timestamp":1759941336383},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642117466"},{"type":"electronic","value":"9783642117473"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11747-3_13","type":"book-chapter","created":{"date-parts":[[2010,1,25]],"date-time":"2010-01-25T01:03:02Z","timestamp":1264381382000},"page":"166-181","source":"Crossref","is-referenced-by-count":15,"title":["Formal Verification of Application-Specific Security Properties in a Model-Driven Approach"],"prefix":"10.1007","author":[{"given":"Nina","family":"Moebius","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kurt","family":"Stenzel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"13_CR1","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M. Burrows","year":"1990","unstructured":"Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Transactions on Computer Systems\u00a08(1), 18\u201336 (1990)","journal-title":"ACM Transactions on Computer Systems"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-45418-7_3","volume-title":"Smart Card Programming and Security","author":"G. Bella","year":"2001","unstructured":"Bella, G.: Mechanising a Protocol for Smart Cards. In: Attali, S., Jensen, T. (eds.) E-smart 2001. LNCS, vol.\u00a02140, p. 19. Springer, Heidelberg (2001)"},{"issue":"4","key":"13_CR3","doi-asserted-by":"crossref","first-page":"363","DOI":"10.3233\/JCS-2009-0339","volume":"17","author":"B. Blanchet","year":"2009","unstructured":"Blanchet, B.: Automatic Verification of Correspondences for Security Protocols. Journal of Computer Security\u00a017(4), 363\u2013434 (2009)","journal-title":"Journal of Computer Security"},{"issue":"1-2","key":"13_CR4","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10817-005-9018-6","volume":"36","author":"G. Bella","year":"2006","unstructured":"Bella, G., Massacci, F., Paulson, L.C.: Verifying the SET purchase protocols. Journal of Automated Reasoning\u00a036(1-2), 5\u201337 (2006)","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"13_CR5","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"D.A. Basin","year":"2005","unstructured":"Basin, D.A., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: A symbolic model checker for security protocols. Int. J. Inf. Sec.\u00a04(3), 181\u2013208 (2005)","journal-title":"Int. J. Inf. Sec."},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-46428-X_25","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Balser","year":"2000","unstructured":"Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, p. 363. Springer, Heidelberg (2000)"},{"key":"13_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines\u2014A Method for High-Level System Design and Analysis","author":"E. B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines\u2014A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)"},{"key":"13_CR8","volume-title":"Proc. 22th IEEE Symposium on Foundations of Computer Science","author":"D. Dolev","year":"1981","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. In: Proc. 22th IEEE Symposium on Foundations of Computer Science. IEEE, Los Alamitos (1981)"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-540-73210-5_17","volume-title":"Integrated Formal Methods","author":"D. Haneberg","year":"2007","unstructured":"Haneberg, D., Grandy, H., Reif, W., Schellhorn, G.: Verifying Smart Card Applications: An ASM Approach. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 313\u2013332. Springer, Heidelberg (2007)"},{"key":"13_CR10","volume-title":"Secure Systems Development with UML","author":"J. J\u00fcrjens","year":"2005","unstructured":"J\u00fcrjens, J.: Secure Systems Development with UML. Springer, Heidelberg (2005)"},{"key":"13_CR11","unstructured":"J\u00fcrjens, J.: Developing high-assurance secure systems with UML: a smartcard-based purchase protocol. In: IEEE International Symposium on High Assurance Systems Engineering (2004)"},{"volume-title":"Formal Aspects of Computing","year":"2008","key":"13_CR12","unstructured":"Jones, C., Woodcock, J. (eds.): Formal Aspects of Computing, vol.\u00a020 (1). Springer, Heidelberg (2008)"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"issue":"2","key":"13_CR14","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming\u00a026(2), 113\u2013131 (1996)","journal-title":"Journal of Logic Programming"},{"key":"13_CR15","volume-title":"Third International Workshop on Secure Software Engineering, SecSE, at ARES 2009","author":"N. Moebius","year":"2009","unstructured":"Moebius, N., Stenzel, K., Grandy, H., Reif, W.: SecureMDD: A Model-Driven Development Method for Secure Smart Card Applications. In: Third International Workshop on Secure Software Engineering, SecSE, at ARES 2009. IEEE Press, Los Alamitos (2009)"},{"key":"13_CR16","unstructured":"Moebius, N., Stenzel, K., Reif, W.: Modeling Security-Critical Applications with UML in the SecureMDD Approach. International Journal on Advances in Software\u00a01(1) (2008)"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Moebius, N., Stenzel, K., Reif, W.: Generating Formal Specifications for Security-Critical Applications - A Model-Driven Approach. In: ICSE 2009 Workshop: International Workshop on Software Engineering for Secure Systems (SESS 2009). IEEE\/ACM Digital Libary (2009)","DOI":"10.1109\/IWSESS.2009.5068461"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: The Inductive Approach to Verifying Cryptographic Protocols. J. Computer Security\u00a06 (1998)","DOI":"10.3233\/JCS-1998-61-205"},{"key":"13_CR19","unstructured":"Lopez Pimental, J.C., Monroy, R.: Formal support to security protocol development: A survey. Computacion y Sistemas\u00a012(1) (2008)"},{"issue":"10","key":"13_CR20","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1109\/MC.2006.340","volume":"39","author":"J. Woodcock","year":"2006","unstructured":"Woodcock, J.: First Steps in the Verified Software Grand Challenge. IEEE Computer\u00a039(10), 57\u201364 (2006)","journal-title":"IEEE Computer"}],"container-title":["Lecture Notes in Computer Science","Engineering Secure Software and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11747-3_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:43:28Z","timestamp":1606185808000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11747-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642117466","9783642117473"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11747-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}