| changeset 65538 | a39ef48fbee0 |
| parent 61830 | 4f5ab843cf5b |
| 65537:7ce5fcebfb35 | 65538:a39ef48fbee0 |
|---|---|
4 |
4 |
5 section \<open>Smartcard protocols: rely on conventional Message and on new EventSC and Smartcard\<close> |
5 section \<open>Smartcard protocols: rely on conventional Message and on new EventSC and Smartcard\<close> |
6 |
6 |
7 theory Auth_Smartcard |
7 theory Auth_Smartcard |
8 imports |
8 imports |
9 "ShoupRubin" |
9 ShoupRubin |
10 "ShoupRubinBella" |
10 ShoupRubinBella |
11 begin |
11 begin |
12 |
12 |
13 end |
13 end |