equal
deleted
inserted
replaced
33 \<close> |
33 \<close> |
34 |
34 |
35 type_synonym key = nat |
35 type_synonym key = nat |
36 consts invKey :: "key \<Rightarrow> key" |
36 consts invKey :: "key \<Rightarrow> key" |
37 (*<*) |
37 (*<*) |
38 consts all_symmetric :: bool \<comment>\<open>true if all keys are symmetric\<close> |
38 consts all_symmetric :: bool \<comment> \<open>true if all keys are symmetric\<close> |
39 |
39 |
40 specification (invKey) |
40 specification (invKey) |
41 invKey [simp]: "invKey (invKey K) = K" |
41 invKey [simp]: "invKey (invKey K) = K" |
42 invKey_symmetric: "all_symmetric --> invKey = id" |
42 invKey_symmetric: "all_symmetric --> invKey = id" |
43 by (rule exI [of _ id], auto) |
43 by (rule exI [of _ id], auto) |
86 "\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" |
86 "\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" |
87 "\<lbrace>x, y\<rbrace>" == "CONST MPair x y" |
87 "\<lbrace>x, y\<rbrace>" == "CONST MPair x y" |
88 |
88 |
89 |
89 |
90 definition keysFor :: "msg set => key set" where |
90 definition keysFor :: "msg set => key set" where |
91 \<comment>\<open>Keys useful to decrypt elements of a message set\<close> |
91 \<comment> \<open>Keys useful to decrypt elements of a message set\<close> |
92 "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}" |
92 "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}" |
93 |
93 |
94 |
94 |
95 subsubsection\<open>Inductive Definition of All Parts" of a Message\<close> |
95 subsubsection\<open>Inductive Definition of All Parts" of a Message\<close> |
96 |
96 |