author | wenzelm |
Thu, 10 Dec 2015 21:39:33 +0100 | |
changeset 61830 | 4f5ab843cf5b |
parent 58889 | 5b7a9633cfa8 |
child 65538 | a39ef48fbee0 |
permissions | -rw-r--r-- |
32632 | 1 |
(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
1944 | 2 |
Copyright 1996 University of Cambridge |
3 |
*) |
|
4 |
||
61830 | 5 |
section \<open>Blanqui's "guard" concept: protocol-independent secrecy\<close> |
1944 | 6 |
|
32632 | 7 |
theory Auth_Guard_Public |
8 |
imports |
|
9 |
"P1" |
|
10 |
"P2" |
|
11 |
"Guard_NS_Public" |
|
12 |
"Proto" |
|
13 |
begin |
|
14145
2e31b8cc8788
ZhouGollmann: new example (fair non-repudiation protocol)
paulson
parents:
13922
diff
changeset
|
14 |
|
32632 | 15 |
end |