equal
deleted
inserted
replaced
1 (* Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
1 (* Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Copyright 1996 University of Cambridge |
2 Copyright 1996 University of Cambridge |
3 *) |
3 *) |
4 |
4 |
5 header {* Blanqui's "guard" concept: protocol-independent secrecy *} |
5 section {* Blanqui's "guard" concept: protocol-independent secrecy *} |
6 |
6 |
7 theory Auth_Guard_Public |
7 theory Auth_Guard_Public |
8 imports |
8 imports |
9 "P1" |
9 "P1" |
10 "P2" |
10 "P2" |