| changeset 41413 | 64cd30d6b0b8 |
| parent 39246 | 9e58f0499f57 |
| child 41774 | 13b97824aec6 |
| 41412:35f30e07fe0d | 41413:64cd30d6b0b8 |
|---|---|
2 *) |
2 *) |
3 |
3 |
4 header{*Theory of smartcards*} |
4 header{*Theory of smartcards*} |
5 |
5 |
6 theory Smartcard |
6 theory Smartcard |
7 imports EventSC All_Symmetric |
7 imports EventSC "../All_Symmetric" |
8 begin |
8 begin |
9 |
9 |
10 text{* |
10 text{* |
11 As smartcards handle long-term (symmetric) keys, this theoy extends and |
11 As smartcards handle long-term (symmetric) keys, this theoy extends and |
12 supersedes theory Private.thy |
12 supersedes theory Private.thy |