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 newest generation of smart cards will have 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 opens attractives venues and enables convenient applications, but at the same time it poses many 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 and model checkers.
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 focus. |
