equal
deleted
inserted
replaced
3 Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson |
3 Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson |
4 *) |
4 *) |
5 |
5 |
6 header{*The SET Merchant Registration Protocol*} |
6 header{*The SET Merchant Registration Protocol*} |
7 |
7 |
8 theory Merchant_Registration = PublicSET: |
8 theory Merchant_Registration imports PublicSET begin |
9 |
9 |
10 text{*Copmpared with Cardholder Reigstration, @{text KeyCryptKey} is not |
10 text{*Copmpared with Cardholder Reigstration, @{text KeyCryptKey} is not |
11 needed: no session key encrypts another. Instead we |
11 needed: no session key encrypts another. Instead we |
12 prove the "key compromise" theorems for sets KK that contain no private |
12 prove the "key compromise" theorems for sets KK that contain no private |
13 encryption keys (@{term "priEK C"}). *} |
13 encryption keys (@{term "priEK C"}). *} |