equal
deleted
inserted
replaced
50 definition symKeys :: "key set" where |
50 definition symKeys :: "key set" where |
51 "symKeys == {K. invKey K = K}" |
51 "symKeys == {K. invKey K = K}" |
52 |
52 |
53 text{*Agents. We allow any number of certification authorities, cardholders |
53 text{*Agents. We allow any number of certification authorities, cardholders |
54 merchants, and payment gateways.*} |
54 merchants, and payment gateways.*} |
55 datatype_new |
55 datatype |
56 agent = CA nat | Cardholder nat | Merchant nat | PG nat | Spy |
56 agent = CA nat | Cardholder nat | Merchant nat | PG nat | Spy |
57 |
57 |
58 text{*Messages*} |
58 text{*Messages*} |
59 datatype_new |
59 datatype |
60 msg = Agent agent --{*Agent names*} |
60 msg = Agent agent --{*Agent names*} |
61 | Number nat --{*Ordinary integers, timestamps, ...*} |
61 | Number nat --{*Ordinary integers, timestamps, ...*} |
62 | Nonce nat --{*Unguessable nonces*} |
62 | Nonce nat --{*Unguessable nonces*} |
63 | Pan nat --{*Unguessable Primary Account Numbers (??)*} |
63 | Pan nat --{*Unguessable Primary Account Numbers (??)*} |
64 | Key key --{*Crypto keys*} |
64 | Key key --{*Crypto keys*} |