{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:19:01Z","timestamp":1742959141660,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540336891"},{"type":"electronic","value":"9783540336914"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11741060_9","type":"book-chapter","created":{"date-parts":[[2006,4,27]],"date-time":"2006-04-27T09:42:07Z","timestamp":1146130927000},"page":"155-173","source":"Crossref","is-referenced-by-count":5,"title":["Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method"],"prefix":"10.1007","author":[{"given":"Santiago Zanella","family":"B\u00e9guelin","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","volume-title":"Smart Card Handbook","author":"W. Rankl","year":"2000","unstructured":"Rankl, W., Effing, W.: Smart Card Handbook, 2nd edn. John Wiley & Sons, Inc., Chichester (2000)","edition":"2"},{"key":"9_CR2","unstructured":"GlobalPlatform: Card Specification. Version 2.1.1 (2003)"},{"key":"9_CR3","unstructured":"GlobalPlatform, \n                  \n                    http:\/\/www.globalplatform.org"},{"key":"9_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book - Assigning Programs to Meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"9_CR5","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Upper Saddle River (1976)"},{"key":"9_CR6","unstructured":"Site B Grenoble, \n                  \n                    http:\/\/www-lsr.imag.fr\/B\/b-tools.html"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48119-2_22","volume-title":"FM\u201999 - Formal Methods","author":"P. Behm","year":"1999","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.M.: METEOR: A successful application of B in a large project. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 369\u2013387. Springer, Heidelberg (1999)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-60973-3_81","volume-title":"FME \u201996: Industrial Benefit and Advances in Formal Methods","author":"J. Hoare","year":"1996","unstructured":"Hoare, J., Dick, J., Neilson, D., Sorensen, I.: Applying the B technologies to CICS. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol.\u00a01051, pp. 74\u201384. Springer, Heidelberg (1996)"},{"key":"9_CR9","unstructured":"Lanet, J.L., Requet, A.: Formal proof of smart card applets correctness. In: Quisquater, J.J., Schneier, B. (eds.) Third Smart Card Research and Advanced Application Conference, Louvain-la-Neuve, Belgium (1998)"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-540-45236-2_7","volume-title":"FME 2003: Formal Methods","author":"D. Bert","year":"2003","unstructured":"Bert, D., Boulm, S., Potet, M.L., Requet, A., Voisin, L.: Adaptable translator of B specifications to embedded C programs. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 94\u2013113. Springer, Heidelberg (2003)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-48119-2_21","volume-title":"FM\u201999 - Formal Methods","author":"D. Sabatier","year":"1999","unstructured":"Sabatier, D., Lartigue, P.: The use of the B formal method for the design and the validation of the transaction mechanism for smart card applications. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 348\u2013368. Springer, Heidelberg (1999)"},{"key":"9_CR12","unstructured":"Lanet, J.L., Lartigue, P.: The use of formal methods for smartcards, a comparison between B and SDL to model the T=1 protocol. In: Proceedings of International Workshop on Comparing Systems Specification Techniques, Nantes (1998)"},{"key":"9_CR13","first-page":"51","volume-title":"DSN 2002: Proceedings of the 2002 International Conference on Dependable Systems and Networks","author":"L. Casset","year":"2002","unstructured":"Casset, L., Burdy, L., Requet, A.: Formal development of an embedded verifier for Java Card byte code. In: DSN 2002: Proceedings of the 2002 International Conference on Dependable Systems and Networks, Washington, DC, USA, pp. 51\u201358. IEEE Computer Society, Los Alamitos (2002)"},{"key":"9_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-1494-9","volume-title":"The B Language and Method: A guide to Practical Formal Development","author":"K. Lano","year":"1996","unstructured":"Lano, K.: The B Language and Method: A guide to Practical Formal Development. Springer, London (1996)"},{"key":"9_CR15","unstructured":"GlobalPlatform: Card Security Requirements Specification. Version 1.0 (2001)"},{"key":"9_CR16","unstructured":"Manoranjan, M., Satpathy, M., Butler, M.: ProTest: An automatic test environment for B specifications. In: Proceedings of International workshop on Model Based Testing. ECS University of Southhampton (2004)"},{"key":"9_CR17","unstructured":"Ambert, F., Bouquet, F., Chemin, S., Guenaud, S., Legeard, B., Peureux, F., Vacelet, N., Utting, M.: BZ-TT: A tool-set for test generation from Z and B using constraint logic programming. In: Proc. of Formal Approaches to Testing of Software, FATES 2002, pp. 105\u2013120 (2002)"},{"key":"9_CR18","unstructured":"Stepney, S., Cooper, D., Woodcock, J.: An electronic purse: Specification, refinement and proof. Technical Monograph PRG-126, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK (2000)"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/3-540-45614-7_16","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"N. Cata\u00f1o","year":"2002","unstructured":"Cata\u00f1o, N., Huisman, M.: Formal specification and static checking of Gemplus\u2019 electronic purse using ESC\/Java. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 272\u2013289. Springer, Heidelberg (2002)"},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/s10270-004-0058-x","volume":"4","author":"W. Ahrendt","year":"2005","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Software and System Modeling\u00a04, 32\u201354 (2005)","journal-title":"Software and System Modeling"},{"key":"9_CR21","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for certification of Java\/JavaCard programs annotated in JML. J. Log. Algebr. Program.\u00a058, 89\u2013106 (2004)","journal-title":"J. Log. Algebr. Program."},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-540-45236-2_24","volume-title":"FME 2003: Formal Methods","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Requet, A., Lanet, J.L.: Java applet correctness: A developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 422\u2013439. Springer, Heidelberg (2003)"},{"key":"9_CR23","unstructured":"VerifiCard project, \n                  \n                    http:\/\/www.cs.ru.nl\/VerifiCard"},{"key":"9_CR24","unstructured":"Bali project, \n                  \n                    http:\/\/isabelle.in.tum.de\/bali"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/3-540-45309-1_20","volume-title":"Programming Languages and Systems","author":"G. Barthe","year":"2001","unstructured":"Barthe, G., Dufay, G., Jakubiec, L., Serpette, B.P., de Sousa, S.M.: A formal executable semantics of the JavaCard platform. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, pp. 302\u2013319. Springer, Heidelberg (2001)"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Syntax and Semantics of Java","year":"1999","unstructured":"Alves-Foss, J. (ed.): Formal Syntax and Semantics of Java. LNCS, vol.\u00a01523. Springer, Heidelberg (1999)"},{"key":"9_CR27","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-0-387-35528-3_8","volume-title":"Fourth Smart Card Research and Advanced Application Conference (CARDIS 2000)","author":"E. Poll","year":"2000","unstructured":"Poll, E., van den Berg, J., Jacobs, B.: Specification of the JavaCard API in JML. In: Domingo-Ferrer, J., Chan, D., Watson, A. (eds.) Fourth Smart Card Research and Advanced Application Conference (CARDIS 2000), pp. 135\u2013154. Kluwer Acad. Publ., Dordrecht (2000)"},{"key":"9_CR28","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1016\/S1389-1286(01)00163-3","volume":"36","author":"E. Poll","year":"2001","unstructured":"Poll, E., van den Berg, J., Jacobs, B.: Formal specification of the JavaCard API in JML: the APDU class. Computer Networks\u00a036, 407\u2013421 (2001)","journal-title":"Computer Networks"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/3-540-45418-7_14","volume-title":"Smart Card Programming and Security","author":"H. Meijer","year":"2001","unstructured":"Meijer, H., Poll, E.: Towards a full formal specification of the Java Card API. In: Attali, S., Jensen, T. (eds.) E-smart 2001. LNCS, vol.\u00a02140, p. 165. Springer, Heidelberg (2001)"},{"key":"9_CR30","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M.D., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. STTT\u00a07, 212\u2013232 (2005)","journal-title":"STTT"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-45165-X_11","volume-title":"Java on Smart Cards: Programming and Security","author":"E. Poll","year":"2001","unstructured":"Poll, E., van den Berg, J., Jacobs, B.: Formal specification and verification of JavaCard\u2019s application identifier class. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol.\u00a02041, pp. 137\u2013150. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Construction and Analysis of Safe, Secure, and Interoperable Smart Devices"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11741060_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:26:34Z","timestamp":1558272394000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11741060_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540336891","9783540336914"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/11741060_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}