equal
deleted
inserted
replaced
1 (* Title: HOL/Auth/KerberosV.thy |
1 (* Title: HOL/Auth/KerberosV.thy |
2 Author: Giampaolo Bella, Catania University |
2 Author: Giampaolo Bella, Catania University |
3 *) |
3 *) |
4 |
4 |
5 header{*The Kerberos Protocol, Version V*} |
5 section{*The Kerberos Protocol, Version V*} |
6 |
6 |
7 theory KerberosV imports Public begin |
7 theory KerberosV imports Public begin |
8 |
8 |
9 text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*} |
9 text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*} |
10 |
10 |