equal
deleted
inserted
replaced
1 (* Title: HOL/Auth/Kerberos_BAN_Gets.thy |
1 (* Title: HOL/Auth/Kerberos_BAN_Gets.thy |
2 Author: Giampaolo Bella, Catania University |
2 Author: Giampaolo Bella, Catania University |
3 *) |
3 *) |
4 |
4 |
5 header{*The Kerberos Protocol, BAN Version, with Gets event*} |
5 section{*The Kerberos Protocol, BAN Version, with Gets event*} |
6 |
6 |
7 theory Kerberos_BAN_Gets imports Public begin |
7 theory Kerberos_BAN_Gets imports Public begin |
8 |
8 |
9 text{*From page 251 of |
9 text{*From page 251 of |
10 Burrows, Abadi and Needham (1989). A Logic of Authentication. |
10 Burrows, Abadi and Needham (1989). A Logic of Authentication. |