Formal Methods in the Software Life Cycle: Applications

[ main | background | applications | schedule | deliverables ]

There will be four groups, each implementing a different smart card application. Each of these applications involves one smart card applet and one or more terminals that this applet interacts with. (By "terminal" here we do not mean the physical card reader, but the software behind that which takes care of the interaction with the smart cards.)

Note that these terminals may be connected to - or be part of - physical devices such as a cash register, petrol pump, or car. For testing purposes, you will also have to develop rudimentary simulations of these devices. You are free to use any convenient way to integrate terminals and these (simulations of) devices, and to define convenient interfaces between them.

Assignment 1: E-Purse

Design and implement an electronic purse á la the Chipknip. This application consists of:

The balance of the E-purse applet can be creditted at the reload terminal only. In a store the card can be debitted at a POS.

The card should authenticate the reload terminal (only "valid" reload terminals are allowed to increase the balance). The POS should authenticate the card (payment is only possible with "valid" cards). When the keys on one card are compromised, the system as a whole should still be safe.

Assignment 2: Loyalty Card

A supermarket wants to give its customers bonus cards so that they can collect loyalty points when they buy items at the store. Design and implement a loyalty application, á la Airmiles. This application consists of:

The loyalty applet keeps track of the balance of loyalty points saved, and the POS can instruct the applet to add or remove loyalty points. Obviously, customers should not be able to increase their balance unless they buy products at the store.

Assignment 3: Rental Car

A Car Rental firm is planning to use smart cards for several purposes. Each customer is given a smartcard. The smart card is used to identify the customer (with respect to the customer administration data base), but it is also used as an ignition key, and keeps track of the mileage during driving.

Design and implement such a system. The system consists of:

Assignment 4: Petrol Rationing

Due to the unfortunate outcome of a war somewhere in the Middle East, the government has found it necessary to introduce a rationing scheme for petrol, where all car owners receive a fixed monthly petrol allowance.

Design and implement a smartcard-based petrol rationing scheme. This application should consist of:

All car owners are given a petrol rationing smart card that keeps track of how much of their petrol allowance they still have. All petrol pumps are equipped with card terminals, and will only supply petrol upon presentation of a petrol rationing smart card, and subtract the amount of petrol supplied from the allowance on that card. There are special terminals for charging rationing cards. Inserting the card in a charging terminal will increase the allowance by the fixed monthly allowance - provided the card hasn't been charged already that month.