equal
deleted
inserted
replaced
44 |
44 |
45 |
45 |
46 text{*The inverse of a symmetric key is itself; that of a public key |
46 text{*The inverse of a symmetric key is itself; that of a public key |
47 is the private key and vice versa*} |
47 is the private key and vice versa*} |
48 |
48 |
49 constdefs |
49 definition symKeys :: "key set" where |
50 symKeys :: "key set" |
|
51 "symKeys == {K. invKey K = K}" |
50 "symKeys == {K. invKey K = K}" |
52 (*>*) |
51 (*>*) |
53 |
52 |
54 text {* |
53 text {* |
55 Datatype |
54 Datatype |
90 translations |
89 translations |
91 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
90 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
92 "{|x, y|}" == "CONST MPair x y" |
91 "{|x, y|}" == "CONST MPair x y" |
93 |
92 |
94 |
93 |
95 constdefs |
94 definition keysFor :: "msg set => key set" where |
96 keysFor :: "msg set => key set" |
|
97 --{*Keys useful to decrypt elements of a message set*} |
95 --{*Keys useful to decrypt elements of a message set*} |
98 "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}" |
96 "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}" |
99 |
97 |
100 |
98 |
101 subsubsection{*Inductive Definition of All Parts" of a Message*} |
99 subsubsection{*Inductive Definition of All Parts" of a Message*} |