equal
deleted
inserted
replaced
1 (* Title: HOL/Auth/OtwayReesBella.thy |
1 (* Title: HOL/Auth/OtwayReesBella.thy |
2 Author: Giampaolo Bella, Catania University |
2 Author: Giampaolo Bella, Catania University |
3 *) |
3 *) |
4 |
4 |
5 header{*Bella's version of the Otway-Rees protocol*} |
5 section{*Bella's version of the Otway-Rees protocol*} |
6 |
6 |
7 |
7 |
8 theory OtwayReesBella imports Public begin |
8 theory OtwayReesBella imports Public begin |
9 |
9 |
10 text{*Bella's modifications to a version of the Otway-Rees protocol taken from |
10 text{*Bella's modifications to a version of the Otway-Rees protocol taken from |