39 | MPair msg msg |
39 | MPair msg msg |
40 | Crypt key msg |
40 | Crypt key msg |
41 |
41 |
42 (*Allows messages of the form {|A,B,NA|}, etc...*) |
42 (*Allows messages of the form {|A,B,NA|}, etc...*) |
43 syntax |
43 syntax |
44 "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") |
44 "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") |
45 |
45 |
46 translations |
46 translations |
47 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
47 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
48 "{|x, y|}" == "MPair x y" |
48 "{|x, y|}" == "MPair x y" |
49 |
49 |
50 |
50 |
51 constdefs |
51 constdefs |
52 (*Message Y, paired with a MAC computed with the help of X*) |
52 (*Message Y, paired with a MAC computed with the help of X*) |
53 HPair :: "[msg,msg]=>msg" |
53 HPair :: "[msg,msg]=>msg" ("(4Hash[_] /_)" [0, 1000]) |
54 "HPair X Y == {| Hash{|X,Y|}, Y|}" |
54 "Hash[X] Y == {| Hash{|X,Y|}, Y|}" |
55 |
55 |
56 (*Keys useful to decrypt elements of a message set*) |
56 (*Keys useful to decrypt elements of a message set*) |
57 keysFor :: msg set => key set |
57 keysFor :: msg set => key set |
58 "keysFor H == invKey `` {K. EX X. Crypt K X : H}" |
58 "keysFor H == invKey `` {K. EX X. Crypt K X : H}" |
59 |
59 |