[Impressum]
[E-Mail]
Modeling a simple Copy Card (3)
The last step is a detailed description of the identified protocols
with UML Activity diagrams that contain checks and status updates.
- getBalance: It it always possible to see the balance on the card, no PIN is required. However,
the state of the card is reset to idle.
- load: Loading money/points onto the card requires an authentic terminal. Authentication
is based on a shared secret known to all terminals and cards, the passphrase.
Replays are avoided by a challenge-response step in advance of the actual load step, and
the state guarantees that the nonce is really fresh.
The passphrase is used in a hash (similar to the key in an HMAC) that also guarantees
that the value to load is not modified.
The terminal keeps track of the real money inserted by the user by adding its value
to its money field.
This can be used to formulate the main security property for the application.
- pay: In a pay step the terminal must be sure that the card is authentic and that
the value on the card is really decreased. Therefore we use a challenge from terminal to card.
Authentication itself is done in the same manner as in the load step.
Note that the load and pay message essentially contain the same data. They are distinguished
by inclusion of a tag, either LOAD or PAY. After the points have been collected
from the card the terminal will issue copies. Before issuing copies the requested value is
subtracted from the money field.
