equal
deleted
inserted
replaced
55 HPair :: "[msg,msg]=>msg" ("(4Hash[_] /_)" [0, 1000]) |
55 HPair :: "[msg,msg]=>msg" ("(4Hash[_] /_)" [0, 1000]) |
56 "Hash[X] Y == {| Hash{|X,Y|}, Y|}" |
56 "Hash[X] Y == {| Hash{|X,Y|}, Y|}" |
57 |
57 |
58 (*Keys useful to decrypt elements of a message set*) |
58 (*Keys useful to decrypt elements of a message set*) |
59 keysFor :: msg set => key set |
59 keysFor :: msg set => key set |
60 "keysFor H == invKey `` {K. EX X. Crypt K X : H}" |
60 "keysFor H == invKey ` {K. EX X. Crypt K X : H}" |
61 |
61 |
62 (** Inductive definition of all "parts" of a message. **) |
62 (** Inductive definition of all "parts" of a message. **) |
63 |
63 |
64 consts parts :: msg set => msg set |
64 consts parts :: msg set => msg set |
65 inductive "parts H" |
65 inductive "parts H" |