author | huffman |
Sun, 25 Mar 2012 20:15:39 +0200 | |
changeset 47108 | 2a1953f0d20d |
parent 32631 | 2489e3c3562b |
child 61830 | 4f5ab843cf5b |
permissions | -rw-r--r-- |
32631 | 1 |
theory All_Symmetric |
2 |
imports Message |
|
3 |
begin |
|
1944 | 4 |
|
32631 | 5 |
text {* All keys are symmetric *} |
1944 | 6 |
|
32631 | 7 |
defs all_symmetric_def: "all_symmetric \<equiv> True" |
14145
2e31b8cc8788
ZhouGollmann: new example (fair non-repudiation protocol)
paulson
parents:
13922
diff
changeset
|
8 |
|
32631 | 9 |
lemma isSym_keys: "K \<in> symKeys" |
10 |
by (simp add: symKeys_def all_symmetric_def invKey_symmetric) |
|
18886 | 11 |
|
32631 | 12 |
end |