equal
deleted
inserted
replaced
35 |
35 |
36 |
36 |
37 subsection{*Basic properties of shrK*} |
37 subsection{*Basic properties of shrK*} |
38 |
38 |
39 (*Injectiveness: Agents' long-term keys are distinct.*) |
39 (*Injectiveness: Agents' long-term keys are distinct.*) |
40 declare inj_shrK [THEN inj_eq, iff] |
40 lemmas shrK_injective = inj_shrK [THEN inj_eq] |
|
41 declare shrK_injective [iff] |
41 |
42 |
42 lemma invKey_K [simp]: "invKey K = K" |
43 lemma invKey_K [simp]: "invKey K = K" |
43 apply (insert isSym_keys) |
44 apply (insert isSym_keys) |
44 apply (simp add: symKeys_def) |
45 apply (simp add: symKeys_def) |
45 done |
46 done |