[Impressum] [E-Mail]

Debitcard

Debitcard is a banking system where a card holder who knows the PIN of his card can withdraw money
from an ATM or use a PC with internet connection to transfer money from one account to another.
The application consists of two kinds of banks: an affiliated bank with multiple ATMs and a direct bank
that can only be reached via a network, e.g. the internet or an ATM of an affiliated bank.

This system application is obviously security-critical. To secure the exchanged messages it uses standard protocols like TLS if possible
but also self-defined protocols if not. This example combines smart cards and services in one application.

Because the most business security requirements can not be mapped on standard security properties, our approach is to prove application-specific security properties.
For this banking system some properties are:
- No money can be lost (more precise: The sum of all account balances plus the amount of all the money that has been withdrawn from cash machines is constant)
- A transfer that is made by an account owner will be debited from his account and credited on the target account that is choosen by the account owner who made the transfer.
- Only the account owner can make a transfer from his account.


Begin the walkthrough

Jump to selected documents

• Sequence diagrams
• Class and Deployment diagrams
• Activity diagram: withdraw money from an ATM
• Activity diagram: transfer money from one account to another
• Generated source code 
• Generated formal model with proofs