equal
deleted
inserted
replaced
1117 Says C M {|{|sign (priSK C) MsgDualSign, |
1117 Says C M {|{|sign (priSK C) MsgDualSign, |
1118 EXcrypt KC EKj {|PIHead, Hash OIData|} PANData|}, |
1118 EXcrypt KC EKj {|PIHead, Hash OIData|} PANData|}, |
1119 OIData, Hash PIData|} |
1119 OIData, Hash PIData|} |
1120 \<in> set evs" |
1120 \<in> set evs" |
1121 apply clarify |
1121 apply clarify |
|
1122 apply hypsubst_thin |
1122 apply (erule rev_mp) |
1123 apply (erule rev_mp) |
1123 apply (erule rev_mp) |
1124 apply (erule rev_mp) |
1124 apply (erule set_pur.induct, simp_all, auto) |
1125 apply (erule set_pur.induct, simp_all, auto) |
1125 done |
1126 done |
1126 |
1127 |