equal
deleted
inserted
replaced
46 |
46 |
47 |
47 |
48 text{*The inverse of a symmetric key is itself; that of a public key |
48 text{*The inverse of a symmetric key is itself; that of a public key |
49 is the private key and vice versa*} |
49 is the private key and vice versa*} |
50 |
50 |
51 constdefs |
51 definition symKeys :: "key set" where |
52 symKeys :: "key set" |
|
53 "symKeys == {K. invKey K = K}" |
52 "symKeys == {K. invKey K = K}" |
54 |
53 |
55 text{*Agents. We allow any number of certification authorities, cardholders |
54 text{*Agents. We allow any number of certification authorities, cardholders |
56 merchants, and payment gateways.*} |
55 merchants, and payment gateways.*} |
57 datatype |
56 datatype |
79 translations |
78 translations |
80 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
79 "{|x, y, z|}" == "{|x, {|y, z|}|}" |
81 "{|x, y|}" == "CONST MPair x y" |
80 "{|x, y|}" == "CONST MPair x y" |
82 |
81 |
83 |
82 |
84 constdefs |
83 definition nat_of_agent :: "agent => nat" where |
85 nat_of_agent :: "agent => nat" |
|
86 "nat_of_agent == agent_case (curry nat2_to_nat 0) |
84 "nat_of_agent == agent_case (curry nat2_to_nat 0) |
87 (curry nat2_to_nat 1) |
85 (curry nat2_to_nat 1) |
88 (curry nat2_to_nat 2) |
86 (curry nat2_to_nat 2) |
89 (curry nat2_to_nat 3) |
87 (curry nat2_to_nat 3) |
90 (nat2_to_nat (4,0))" |
88 (nat2_to_nat (4,0))" |