 |
| Fig. 1: m-commerce trust network |
Security Analysis for Multi-Applet Smart Cards
SAMASC
Dr. B.P.F. Jacobs
Security protocols are essential for providing security. They are sets of rules for the secure exchange of information in insecure environments, based on cryptographic techniques. Smart cards are currently a standard means of providing secure authentication over networks, notably used in all mobile phones (as SIMs) and in many bank cards, and their use for controlling access to network-based services will increase in the near future. The latest generation of smart cards has a simple operating system for the execution of application programs (called applets), written in a Java-like language. Multiple applets may exist on a single card, and may even be added after card issuance. This simplifies the development of applications, and makes interesting new applications possible, but at the same time it poses entirely new security threats, which are complicated in nature because of the many parties that may be involved (and the non-trivial trust relationships that may exist between them).
The innovation of the proposal lies in its aim to analyse security protocols in the context of scenarios for smart cards with multiple applets. The presence of multiple applets adds a completely new dimension with its own security risks. Another innovative aspect of the proposed research is its aim to study security protocols "in context": we do not not just consider the abstract core of a protocol (as is commonly done in most work in the literature), but explicitly include the particular setting in which the protocol is used. The analysis will involve an appropriate combination, and likely extension, of existing techniques from the literature, involving actual verification with theorem provers.
The two main case studies are security of mobile commerce and of applet downloading. The project combines existing expertise in smart cards, security, and formal methods, and strengthens the position of the Netherlands in this important area. In the project there will be light-weighted industrial participation through KPN Research (KPN is the formerly state-owned, national telecommunications provider in the Netherlands. It runs its own research labs, known as KPN Research, see http://www.research.kpn.com/.) guaranteeing appropriate practical focus.
This proposal involves aspects from many disciplines and sub-disciplines used by NWO:
This project also has obvious connections with two of NWO's priority themes:
Within the group Informatics for Technical Applications at the University of Nij\-megen, the "LOOP" subgroup (see http://www.cs.kun.nl/~bart/LOOP/) around Jacobs and Poll has developed into a recognised center of excellence for Java Card based smart cards. Jacobs and Poll are running several projects on smart card correctness, notably coordinating the EU-funded IST-project VerifiCard. The LOOP group is well-known for its contributions to Java program semantics and correctness, using proof tools. A natural extension of this line of research involves security issues related to smart cards. It links the internal organisation of smart cards with their actual use in security sensitive scenarios.
| Name |
hours per week |
specialism |
|---|---|---|
|
Dr. B.P.F. Jacobs (Royal Academy Fellow) |
4 |
semantics, specification & verification for Java(Card); use of proof tools (esp. PVS) |
|
Dr.ir E. Poll (postdoc) |
4 |
program logics and verification tools; formal methods for Java(Card) |
|
Prof.dr. J. Bruijning (part-time professor) |
2 |
head of security expert group at KPN Research |
| Project PhD student | 40 |
The planned promotor of the PhD student is Jacobs (A procedure for a personal chair is foreseen.)
Within the Formal Methods group at the Eindhoven University of Technology (see http://www.win.tue.nl/fm/) there is considerable expertise on, experience with, and access to protocol descriptions and their industrial use scenarios (notably involving their feasibility). Especially De Vink, a former employee of KPN Research, has intimate knowledge of scenarios for smart cards in a commercial setting, and of formal methods (like BAN logic) to describe such scenarios. Mauw is an expert on Message Sequence Charts (MSCs) and on industrial strength specification languages. He contributed to standardization work on MSCs within the International Telecommunications Union (ITU) in Geneva and is external advisor of the Open Card Framework project at Philips Research Labs on the application of settop boxes for secure transaction. Together they form a natural complement to the team from Nijmegen, and are ideally positioned to collaborate on security for smart cards. Also at TU/e there is, in the same faculty in the group of Van Tilborg, in-depth knowledge of and practical experience with cryptanalysis, e.g. powerattacks on smart cards. This expertise could prove useful in later stages of the project.
| Name |
hours per week |
specialism |
|---|---|---|
|
Dr. E. de Vink (lecturer) |
4 |
security in telecom industry; formal methods |
|
Dr. S. Mauw (reader) |
2 |
analysis and design of communication protocols; formal methods |
| Project PhD student | 40 |
The promotor of the PhD student will be Prof. dr. J.C.M. Baeten, head of the Formal Methods group at TU/e.
Both the research groups at the universities of Eindhoven and Nijmegen are part of the national research school Institute for Programming research and Algorithmics (IPA, http://www.win.tue.nl/ipa/). The proposed research largely falls within IPA's main theme Formal Methods, more specifically in the subtheme Semantics and the subtheme Specification, verification and testing.
There is a fundamental tension between the demands placed on ICT-applications today, namely between openness and connectivity on the one hand, and security and reliability on the other. Main-frames, desktop computers, laptops, palmtops, mobile phones etc. are all connected and accessible via networks, be it wired or wireless (as is more and more often the case). This connectivity has become a vital ingredient of our modern society. Also, there is a shift of having software, instead of hardware or humans, as regulator of control, resulting in an increase of flexibility. But all this comes at a high price, as at the same time they result in new vulnerabilities. Confidentiality and authenticity of information that is exchanged between computing machinery is often a necessary precondition in many of these activities. For example, the participation of a large audience in e-commerce is hindered by the lack of trust in the security of the underlying infrastructure. By exploiting software bugs, malicious attackers may gain unprecedented power of disruption, and can create substantial damage within crucial information systems and threaten pivotal interconnectivities. Also, frightening topics such as information warfare have become recurring items on the political agenda. It is widely recognised that security of communications between computers is of paramount importance.
A relatively new discipline within computer science studies security protocols (sometimes also called cryptographic protocols). These protocols are sets of rules for secure exchange of information over insecure network environments, based on cryptographic techniques. Typical goals are integrity and confidentiality of communication, authentication of a partner in a transaction and authorisation and non-repudiation of requests. Security protocols are thus different from transmission protocols, which are concerned with the actual transfer of messages, typically involving fragmentation and error correction, and not with the actual content of the messages that are transferred. As a response to a general concern about security of transactions (especially on the internet), there is a growing integration of cryptographic modules into application programs, protocol stacks and operating systems. A typical example is the currently discussed move from DNS to DNSSEC (the latter extending the functionality of the former by offering security of the provided domain name services).
Security protocols as studied within computer science rely on basic cryptographic techniques, but the actual development of these techniques is not part of the area. For the security analysis the basic cryptographic ingredients of encryption and decryption, signing and verification, collision free hashes, random number and key generation, etc. are considered as black box building blocks. They are used in abstract form, via operations like encrypt and decrypt which work on a message and a key, and produce an encrypted or decrypted message, respectively. The details of these operations are important to establish the cryptographic strength of the protocol. However, crucial for the security is the interplay of transactions based on shared or public keys and on diversification using nonces and time-stamps, and how, and under what conditions their combination will establish the desired transfer of trust, in particular security features as integrity, confidentiality, authenticity and non-repudiation.
An expressive framework to describe security protocols at an adequate level of abstraction and a clear model for their interpretation that allows for tool-supported semantical analysis (including verification), are pivotal for a proper understanding of the security functionality of the protocols. Since the seminal work of Abadi et al. [BurrowsAN89] (on what has become known as BAN logic) several extension of the BAN formalism have been proposed [GNY90,Syv93,WK96] and various security protocols have been analysed in the literature, often resulting in the revealing of flaws and unexpected weaknesses [Lowe96]. Also, in the broader context of standardisation bodies like IETF and ETSI, the security analysis is usually one of the main activities in the design or selection phase for new communication protocols. The number of different scenarios that can possibly arise in such an analysis is typically well-beyond what humans can capture, and therefore formal methods are indispensable for getting a handle on the possible weaknesses. For example, the new standard protocols that are currently being developed for the UMTS wireless communication standard are being formalised using BAN logic (See http://www.3gpp.org/TSG/SA.htm). Also the SET protocol that has been proposed by a consortium of credit card and software companies to protect sensitive card-holder information, in order to ensure payment integrity and to authenticate merchants and card-holders, will be scrutinised with formal methods (See http://www.cl.cam.ac.uk/users/lcp/Grants/SET.html).
Smart cards are plastic cards, the size of a credit card, with a built-in micro-chip. This chip is capable of storing data as well as processing data (notably encrypting and decrypting it). Smart cards communicate with a terminal via byte sequences, following the ISO7816 protocol.
Smart cards are familiar to the general public in the form of bank cards or phone cards. Smart cards provide a means to safely store small amounts of secret data and/or algorithms, and are increasingly used in situations that require authenticated access or secure transactions. Smart cards are starting to be used as loyalty cards, in public transport, and in health care. All mobile phones already contain a smart card (a SIM, Subscriber Identification Module) for authenticated identification of the caller by the network. Smart cards provide a way to control access to computers and networks and can provide the secure and authenticated Internet access useful for e-commerce, m-commerce (with `m' for mobile), on-line banking, etc. Smart card readers are set to become a fairly standard piece of equipment on laptops and PC's, initially mainly as a means to control access to corporate networks. IBM, Compaq, and HP already have PCs that include a smart card reader as standard equipment, and Microsoft predicts that eventually the standard PC keyboard will have a smart card reader built in. Also, there are experimental GSM phones with a smart card reader. These play an important role in the development of new protocols for m-commerce.
The latest generation of smart cards contain a processor capable of executing simple programs, called applets. A special Java dialect, called Java Card, has been developed for programming such smart card applets. Java Card is a stripped-down version of Java, adapted to the limited resources of smart cards as far as memory and computing power is concerned. For instance, Java Card does not support floating point numbers, cloning, or threads. Applets are thus written in a high level language and are designed to run on a standardised open platform. These new smart cards have many important advantages. Cards can hold several applets in their memory at the same time ("multi-application"), and new applets can be added ("downloaded") after the cards have been issued ("post-issuance"), allowing services to be updated or new services to be added without replacing the card. As mentioned earlier, these advantages also create many security risks. The nightmare scenario is a virus on ones smart card. The smart card industry is well-aware of these risks - because security is their product - and is actively collaborating with academia in various forms, see e.g. Verificard. Also, researchers in academia have recognised these smart cards as an appropriate application area for their theories and techniques. In this setting, the current proposal seeks to apply formal methods for security protocols to the new generation of multi-application smart cards with post-issuance downloading.
The new generation of smart cards and the demand for novel services in telecommunications give rise to new scenarios where security is a crucial issue. Typically, these scenarios rely on complicated trust relations between the various parties involved. Especially, each applet is best considered as an entity on its own, trusting the operating system on the card, the (external) party that provided the applet, and possibly some other applet on the same card that is relevant for a particular scenario. This multi-applet aspect is a new ingredient which is not part of earlier investigations [AbadiBKL93,Bella99]. Whereas typical smart cards provide standard encryption algorithms for en- and decrypting the communication between an applet and the outside world, security of communication between applets on a single multi-applet smart card relies on the smart card operating system. Here the smart card operating system provides authentication between the applets, and ensures that communications between two applets on the card cannot be observed by a third party.
There are several tool-supported approaches for general security protocol, amongst others, the NRL Protocol Analyzer of Meadows c.s. [Mea96], the usage of CSP with FDR by Roscoe and Lowe [LR97], the special tools of Kindred and Wing [KW96] and of Dekker [Dek00]. The starting point for the security analysis on smart cards in this project will be the successful work of Paulson [Paulson98] on formalisation of security protocols and their verification using the proof tool Isabelle. In this so-called Inductive Approach induction is used at two different levels:
The scientific aim of the proposed project is to generalise and adapt this inductive approach in order to make it most suitable for security protocols with smart cards. This will involve:
The aim of this re-formalisation is thus to obtain a suitably abstract, expressive, and flexible framework for the state-based modeling of security protocols for smart cards, which can be used for verification with theorem provers (building on the existing expertise and experience of the applicants in this field). The new adapted formalism will be used for two main case studies.
The first case study focuses on the design and verification of the application of multi-applet smart cards in the setting of mobile commerce, where one can purchase goods and/or information via a mobile phone. Also the payment can be arranged via the hand-held device.
|
| Fig. 1: m-commerce trust network |
We start from the assumption that a customer has been authenticated by the telecommunication company upon acquisition of the mobile phone. The telecommunications company knows the link between the SIM for the mobile phone and the identity of the customer. Based on this, the telecommunications company provides authentication information of the SIM in the form of an applet for the applet platform on the mobile phone. Next, in order to facilitate mobile payments, the customer needs to obtain an applet from her bank and have it down-loaded on the mobile phone (post-issuance). A possible solution for the authentication problem of the mobile phone with respect to the bank is the usage of a suitable public key infrastructure (PKI) on which the telecommunications company and the bank agree. Armed with the applet from the bank the customer may for her payments engage, e.g. in a SET-style protocol. See Figure 1.
The main topics to address in this case study are the guarantee of authenticity and non-repudiation and to investigate the feasibility of attacks on the overall protocol. The threats, practicality and advantages of separate cards or multiple applets related to different banks is an important issue here. A number of versions of the protocol, based on different assumptions regarding the trust relations and meeting various user-requirements, will be developed. Also recovery scenarios in case of loss, theft or hardware failures will be part of the case study.
The second case study concerns the downloading (and installing) of applets onto a smart card. The possibility of downloading additional applets on an existing card is not only one of the main benefits of the new generation of smart cards, but is also the main potential security risk (Indeed, post-issuance downloading is disabled on all multi-application smart cards that are currently commercially deployed.). Organisations that issue smart cards will only allow applets they trust to be installed on cards they have issued, just like the organisations that provide these applets will only allow them to be installed on a smart card they trust.
 |
| Fig. 2: Applet download trust network. The dotted lines signify new nodes and connections in the network after downloading. |
The basic infrastructure for downloading and installing applets is specified in the Open Platform standard (Originally developed by Visa (http://www.visa.com/nt/suppliers/open/), and now transferred to GlobalPlatform (http://www.globalplatform.com/).). The three parties involved in downloading an applet are the card issuer, the applet issuer, and the card holder (see Figure 2). Ultimately the card issuer has control over the installation of an applet on a card, but this control can be delegated to the applet issuer, or made subject to approval of the card holder and/or the applet issuer. In this case study, different scenarios for controlling applet download will be investigated.
The main topics to address here are guarantees for the control over applet download by the parties involved, and guarantees that the applet is installed on a particular smart card, essential for authentication of the newly installed applet, notably by its issuer.
If the card holder is asked for approval for downloading an applet, it makes a real difference who controls the channel that is used to communicate the holder's (dis)approval to the card or the card issuer. For instance, if the card is inserted in an ATM owned by the applet issuer, then communications of the card holder to the card or the card issuer (and vice-versa) are visible to the applet issuer; if the smart card is inside the card holder's mobile phone then they are not.
These two case studies both have clear practical relevance and are scientifically challenging: they require integration and further development of existing theories and techniques in the area of security protocols.
[AbadiBKL93]
M. Abadi, M. Burrows, C. Kaufman, and B. Lampson.
Authentication and delegation with smart-cards.
Science of Computer Programming, 21(2):93-113, 1993.
[Bella99]
G. Bella.
Modelling security protocols based on smart cards.
In M. Blum and C.H. Lee, editors, Cryptographic Techniques and
E-Commerce (CrypTEC'99), pages 139-146. City Univ. of Hong Kong Press,
1999.
[BurrowsAN89]
M. Burrows, M. Abadi, and R. Needham.
A logic of authentication.
Proc. Royal Soc., Series A, Volume 426:233-271, 1989.
[Dek00]
A.H. Dekker.
C3po: a tool for automatic sound cryptographic protocol analysis.
In Proc. 13th IEEE Computer Security Foundations Workshop,
2000.
[GNY90]
L. Gong, R. Needham, and R. Yahalom.
Reasoning about belief in cryptographic protocols.
In IEEE Symposium on Research in Security and Privacy, pages
234-248, 1990.
[KW96]
D. Kindred and J.M. Wing.
Fast, automatic checking of security protocols.
In Proc. 2nd USENIX Workshop on Electronic Commerce, pages
41-52, 1996.
[Lowe96]
G. Lowe.
Breaking and fixing the Needham-Schroeder public-key protocol
using CSP and FDR.
In T. Margaria and B. Steffen, editors, Tools and Algorithms for
the Construction and Analysis of Systems, number 1055 in LNCS, pages
147-166. Springer, Berlin, 1996.
[LR97]
G. Lowe and B. Roscoe.
Using CSP to detect errors in the TMN protocols.
IEEE Transactions on Software Engineering, 23:659-669, 1997.
[Mea96]
C. Meadows.
The NRL protocol analyzer: an overview.
Journal of Logic Programming, 26(2):113-131, 1996.
[Paulson98]
L.C. Paulson.
The inductive approach to verifying cryptographic protocols.
Journ. of Computer Security, 6:85-128, 1998.
[Syv93]
P. Syverson.
Adding time to a logic of authentication.
In Proc. 1st ACM Conference on Computer and Communications
Security, pages 97-101, 1993.
[VerificardURL]
EU IST-2000-26328 Project ``VerifiCard''.
http://www.verificard.org/.
[WK96]
G. Wedel and V. Kessler.
Formal semantics for authentication logics.
In Proc. EUSORICS'96, pages 219-241. LNCS 1146, 1996.
The work of the two foreseen PhD students in this project, one in Nijmegen (KUN) and one in Eindhoven (TU/e), will be planned as follows.
During these four years, regular project meetings are foreseen not only with all the participants of the two sites involved (KUN+TU/e), but also with the security experts from KPN Research (Bruijning and experts from his group), ensuring the practical relevance of the project work.
None.
Five important references of the applicants are:
[JacobsBHBHT98]
B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews.
Reasoning about classes in Java (preliminary report).
In Object-Oriented Programming, Systems, Languages and
Applications (OOPSLA), pages 329-340. ACM Press, 1998.
[PollBJ01a]
E. Poll, J. van den Berg, and B. Jacobs.
Formal specification of the JavaCard API in JML: the APDU
class.
Computer Networks, 2001.
To appear. An earlier version appeared in Fourth Smart Card
Research and Advanced Application Conference (IFIP CARDIS'2000), pages
135-154, Kluwer Acad. Publ., 2000.
[HuismanJB00a]
M. Huisman, B. Jacobs, and J. van den Berg.
A case study in class library verification: Java's Vector class.
Techn. Rep. CSI-R0007, Comput. Sci. Inst., Univ. of Nijmegen. To
appear in Software Tools for Technology Transfer, 2001.
[Vin00]
E.P. de Vink (ed.).
OSS Interconnection Gateway Validation, Volume 6: Gateway
Security.
Deliverable EURESCOM Project P908, 2000.
[MaRe98a]
S. Mauw and M.A. Reniers.
Operational semantics for MSC'96.
Computer Networks and ISDN Systems, 31(17):1785-1799, 1999.
Twice the standard budget for a PhD student, kf 228, and travel, kf 7.35. This amounts to kf 470.7 in total.