Abstract
Smart card Web server provides a modern interface between smart cards and the external world. It is of paramount importance that this new software component does not jeopardize the security of the smart card. This paper presents a formal model of the smart card Web server specification and the proof of its security properties. The formalization enables a thoughtful analysis of the specification that has revealed several ambiguities and potentially dangerous behaviors. Our formal model is built using a modular approach upon a model of Java Card and Global Platform. By proving the security properties, we show that the smart card Web server preserves the security policy of the overall model. In other words, this component introduces no illegal access to the card resources (i.e., file system and applications). Furthermore, the smart card Web server provides a means for securely managing the card contents (i.e., resources update).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Affeldt, R., Kobayashi, N.: Formalization and Verification of a Mail Server in Coq. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol. 2609, pp. 217–233. Springer, Heidelberg (2003)
Akhawe, D., Barth, A., Lam, P.E., Mitchell, J.C., Song, D.: Towards a formal foundation of web security. In: Proc. of the 23rd IEEE Computer Security Foundations Symposium, pp. 290–304. IEEE Computer Society (2010)
Barth, A., Jackson, C., Mitchell, J.C.: Securing frame communication in browsers. In: Proc. of 17th USENIX Security Symposium (2008)
Bhargavan, K., Fournet, C., Gordon, A.D.: Verified reference implementations of WS-security protocols. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 88–106. Springer, Heidelberg (2006)
Chetali, B., Nguyen, Q.-H.: Industrial Use of Formal Methods for a High-Level Security Evaluation. In: Cuéllar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 198–213. Springer, Heidelberg (2008)
European Telecommunications Standards Institute. Smart Cards; Application invocation Application Programming Interface (API) by a UICC webserver for Java Card platform, Release 7 (2008), Ref: ETSI TS 102 588, http://pda.etsi.org/pda/queryform.asp
Fu, X., Bultan, T., Su, J.: WSAT: A Tool for Formal Analysis of Web Services. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 510–514. Springer, Heidelberg (2004), available at http://www.cs.ucsb.edu/~su/WSAT/
Global Platform. GlobalPlatform Card Specification 2.2 - Remote Application Management over HTTP - Amendment B, version 0.5 (2008), http://www.globalplatform.org/specificationscard.asp
Haydar, M., Petrenko, A., Sahraoui, H.: Formal Verification of Web Applications Modeled by Communicating Automata. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 115–132. Springer, Heidelberg (2004)
International Organization for Standardization. Identification cards – Integrated circuit(s) cards with contacts. Part 1-11 (1987-2007), http://www.iso.org/
Mitchell, J.C., Shmatikov, V., Stern, U.: Finite-state analysis of ssl 3.0. In: Proc. of 7th USENIX Security Symposium, pp. 201–216 (1998)
Open Mobile Alliance. Smartcard Web Server V1.1 (2009), http://www.openmobilealliance.org/technical/release_program/SCWS_v1_1.aspx
Roscoe, A.W.: Modelling and verifying key-exchange protocols using csp and fdr. In: Proc. of 8th IEEE Computer Security Foundations Workshop, pp. 98–107. IEEE Computer Soc. Press (1995)
Shegalov, G., Weikum, G.: Formal verification of web service interaction contracts. In: Proc. of the 2008 IEEE International Conference on Services Computing, pp. 525–528. IEEE Computer Society (2008)
The Coq Development Team. The Coq Proof Assistant, http://coq.inria.fr/
The Internet Society. HTTP Authentication: Basic and Digest Access Authentication (1999), http://www.ietf.org/rfc/rfc2617.txt
The Internet Society. Hypertext Transfer Protocol – HTTP/1.1 (1999), http://www.ietf.org/rfc/rfc2616.txt
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 IFIP International Federation for Information Processing
About this paper
Cite this paper
Neron, P., Nguyen, QH. (2011). A Formal Security Model of a Smart Card Web Server. In: Prouff, E. (eds) Smart Card Research and Advanced Applications. CARDIS 2011. Lecture Notes in Computer Science, vol 7079. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27257-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-27257-8_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27256-1
Online ISBN: 978-3-642-27257-8
eBook Packages: Computer ScienceComputer Science (R0)