equal
deleted
inserted
replaced
1 (* Title: HOL/Auth/SET/Cardholder_Registration |
1 (* Title: HOL/Auth/SET/Cardholder_Registration |
2 ID: $Id$ |
|
3 Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson, |
2 Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson, |
4 Piero Tramontano |
3 Piero Tramontano |
5 *) |
4 *) |
6 |
5 |
7 header{*The SET Cardholder Registration Protocol*} |
6 header{*The SET Cardholder Registration Protocol*} |
261 THEN set_cr.SET_CR4 [of concl: i C NC2 NCA], |
260 THEN set_cr.SET_CR4 [of concl: i C NC2 NCA], |
262 THEN Says_to_Gets, |
261 THEN Says_to_Gets, |
263 THEN set_cr.SET_CR5 [of concl: C i KC3 NC3 KC2 CardSecret], |
262 THEN set_cr.SET_CR5 [of concl: C i KC3 NC3 KC2 CardSecret], |
264 THEN Says_to_Gets, |
263 THEN Says_to_Gets, |
265 THEN set_cr.SET_CR6 [of concl: i C KC2]]) |
264 THEN set_cr.SET_CR6 [of concl: i C KC2]]) |
266 apply (tactic "PublicSET.basic_possibility_tac") |
265 apply basic_possibility |
267 apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq) |
266 apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq) |
268 done |
267 done |
269 |
268 |
270 text{*General facts about message reception*} |
269 text{*General facts about message reception*} |
271 lemma Gets_imp_Says: |
270 lemma Gets_imp_Says: |