author | wenzelm |
Thu, 09 Mar 2017 14:05:34 +0100 | |
changeset 65158 | b87a972b965d |
parent 62145 | 5b946c81dfbf |
permissions | -rw-r--r-- |
32631 | 1 |
theory All_Symmetric |
2 |
imports Message |
|
3 |
begin |
|
1944 | 4 |
|
61830 | 5 |
text \<open>All keys are symmetric\<close> |
1944 | 6 |
|
62145 | 7 |
overloading all_symmetric \<equiv> all_symmetric |
8 |
begin |
|
9 |
definition "all_symmetric \<equiv> True" |
|
10 |
end |
|
14145
2e31b8cc8788
ZhouGollmann: new example (fair non-repudiation protocol)
paulson
parents:
13922
diff
changeset
|
11 |
|
32631 | 12 |
lemma isSym_keys: "K \<in> symKeys" |
13 |
by (simp add: symKeys_def all_symmetric_def invKey_symmetric) |
|
18886 | 14 |
|
32631 | 15 |
end |