612 \<in> set evs; |
612 \<in> set evs; |
613 Outpts (Card A') A' \<lbrace>Nonce Na, Crypt (crdK (Card A')) (Nonce Na)\<rbrace> |
613 Outpts (Card A') A' \<lbrace>Nonce Na, Crypt (crdK (Card A')) (Nonce Na)\<rbrace> |
614 \<in> set evs; |
614 \<in> set evs; |
615 evs \<in> srb \<rbrakk> \<Longrightarrow> A=A'" |
615 evs \<in> srb \<rbrakk> \<Longrightarrow> A=A'" |
616 apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all) |
616 apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all) |
617 apply (fastsimp dest: Outpts_parts_used) |
617 apply (fastforce dest: Outpts_parts_used) |
618 apply blast |
618 apply blast |
619 done |
619 done |
620 |
620 |
621 (*B's card's output: the NONCE uniquely identifies the rest*) |
621 (*B's card's output: the NONCE uniquely identifies the rest*) |
622 lemma Outpts_B_Card_unique_nonce: |
622 lemma Outpts_B_Card_unique_nonce: |
623 "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key SK, Cert1, Cert2\<rbrace> \<in> set evs; |
623 "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key SK, Cert1, Cert2\<rbrace> \<in> set evs; |
624 Outpts (Card B') B' \<lbrace>Nonce Nb, Agent A', Key SK', Cert1', Cert2'\<rbrace> \<in> set evs; |
624 Outpts (Card B') B' \<lbrace>Nonce Nb, Agent A', Key SK', Cert1', Cert2'\<rbrace> \<in> set evs; |
625 evs \<in> srb \<rbrakk> \<Longrightarrow> B=B' \<and> A=A' \<and> SK=SK' \<and> Cert1=Cert1' \<and> Cert2=Cert2'" |
625 evs \<in> srb \<rbrakk> \<Longrightarrow> B=B' \<and> A=A' \<and> SK=SK' \<and> Cert1=Cert1' \<and> Cert2=Cert2'" |
626 apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all) |
626 apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all) |
627 apply (fastsimp dest: Outpts_parts_used) |
627 apply (fastforce dest: Outpts_parts_used) |
628 apply blast |
628 apply blast |
629 done |
629 done |
630 |
630 |
631 |
631 |
632 (*B's card's output: the SESKEY uniquely identifies the rest*) |
632 (*B's card's output: the SESKEY uniquely identifies the rest*) |
633 lemma Outpts_B_Card_unique_key: |
633 lemma Outpts_B_Card_unique_key: |
634 "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key SK, Cert1, Cert2\<rbrace> \<in> set evs; |
634 "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key SK, Cert1, Cert2\<rbrace> \<in> set evs; |
635 Outpts (Card B') B' \<lbrace>Nonce Nb', Agent A', Key SK, Cert1', Cert2'\<rbrace> \<in> set evs; |
635 Outpts (Card B') B' \<lbrace>Nonce Nb', Agent A', Key SK, Cert1', Cert2'\<rbrace> \<in> set evs; |
636 evs \<in> srb \<rbrakk> \<Longrightarrow> B=B' \<and> A=A' \<and> Nb=Nb' \<and> Cert1=Cert1' \<and> Cert2=Cert2'" |
636 evs \<in> srb \<rbrakk> \<Longrightarrow> B=B' \<and> A=A' \<and> Nb=Nb' \<and> Cert1=Cert1' \<and> Cert2=Cert2'" |
637 apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all) |
637 apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all) |
638 apply (fastsimp dest: Outpts_parts_used) |
638 apply (fastforce dest: Outpts_parts_used) |
639 apply blast |
639 apply blast |
640 done |
640 done |
641 |
641 |
642 lemma Outpts_A_Card_unique_key: |
642 lemma Outpts_A_Card_unique_key: |
643 "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, V\<rbrace> \<in> set evs; |
643 "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, V\<rbrace> \<in> set evs; |
652 (*Revised unicity theorem - applies to both steps 4 and 7*) |
652 (*Revised unicity theorem - applies to both steps 4 and 7*) |
653 lemma Outpts_A_Card_Unique: |
653 lemma Outpts_A_Card_Unique: |
654 "\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk> |
654 "\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk> |
655 \<Longrightarrow> Unique (Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace>) on evs" |
655 \<Longrightarrow> Unique (Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace>) on evs" |
656 apply (erule rev_mp, erule srb.induct, simp_all add: Unique_def) |
656 apply (erule rev_mp, erule srb.induct, simp_all add: Unique_def) |
657 apply (fastsimp dest: Outpts_parts_used) |
657 apply (fastforce dest: Outpts_parts_used) |
658 apply blast |
658 apply blast |
659 apply (fastsimp dest: Outpts_parts_used) |
659 apply (fastforce dest: Outpts_parts_used) |
660 apply blast |
660 apply blast |
661 done |
661 done |
662 |
662 |
663 (*can't prove the same on evs10 for it doesn't have a freshness assumption!*) |
663 (*can't prove the same on evs10 for it doesn't have a freshness assumption!*) |
664 |
664 |
707 \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)), |
707 \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)), |
708 Cert1, Cert3, Cert2\<rbrace> \<in> set evs; |
708 Cert1, Cert3, Cert2\<rbrace> \<in> set evs; |
709 evs \<in> srb \<rbrakk> |
709 evs \<in> srb \<rbrakk> |
710 \<Longrightarrow> Nonce (Pairkey(A,B)) \<in> analz (knows Spy evs)" |
710 \<Longrightarrow> Nonce (Pairkey(A,B)) \<in> analz (knows Spy evs)" |
711 apply (case_tac "A = Spy") |
711 apply (case_tac "A = Spy") |
712 apply (fastsimp dest!: Inputs_imp_knows_Spy_secureM [THEN analz.Inj]) |
712 apply (fastforce dest!: Inputs_imp_knows_Spy_secureM [THEN analz.Inj]) |
713 apply (blast dest!: Pairkey_Inputs_imp_Gets [THEN Pairkey_Gets_analz_knows_Spy]) |
713 apply (blast dest!: Pairkey_Inputs_imp_Gets [THEN Pairkey_Gets_analz_knows_Spy]) |
714 done |
714 done |
715 |
715 |
716 (* This fails on base case because of XOR properties. |
716 (* This fails on base case because of XOR properties. |
717 lemma Pairkey_authentic: |
717 lemma Pairkey_authentic: |
1016 (*Fake*) |
1016 (*Fake*) |
1017 apply spy_analz |
1017 apply spy_analz |
1018 (*Forge*) |
1018 (*Forge*) |
1019 apply (rotate_tac 7) |
1019 apply (rotate_tac 7) |
1020 apply (drule parts.Inj) |
1020 apply (drule parts.Inj) |
1021 apply (fastsimp dest: Outpts_B_Card_form_7) |
1021 apply (fastforce dest: Outpts_B_Card_form_7) |
1022 (*SR_U7*) |
1022 (*SR_U7*) |
1023 apply (blast dest!: Outpts_B_Card_form_7) |
1023 apply (blast dest!: Outpts_B_Card_form_7) |
1024 (*SR_U7F*) |
1024 (*SR_U7F*) |
1025 apply clarify |
1025 apply clarify |
1026 apply (drule Outpts_parts_used) |
1026 apply (drule Outpts_parts_used) |
1027 apply simp |
1027 apply simp |
1028 (*faster than |
1028 (*faster than |
1029 apply (fastsimp dest: Outpts_parts_used) |
1029 apply (fastforce dest: Outpts_parts_used) |
1030 *) |
1030 *) |
1031 (*SR_U10*) |
1031 (*SR_U10*) |
1032 apply (fastsimp dest: Outpts_B_Card_form_7) |
1032 apply (fastforce dest: Outpts_B_Card_form_7) |
1033 (*SR_U10F - uses assumption Card A not cloned*) |
1033 (*SR_U10F - uses assumption Card A not cloned*) |
1034 apply clarify |
1034 apply clarify |
1035 apply (drule Outpts_B_Card_form_7, assumption) |
1035 apply (drule Outpts_B_Card_form_7, assumption) |
1036 apply simp |
1036 apply simp |
1037 (*Oops1*) |
1037 (*Oops1*) |
1343 B \<noteq> Server; B \<noteq> Spy; evs \<in> srb \<rbrakk> |
1343 B \<noteq> Server; B \<noteq> Spy; evs \<in> srb \<rbrakk> |
1344 \<Longrightarrow> \<exists> Cert2 K. |
1344 \<Longrightarrow> \<exists> Cert2 K. |
1345 Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Certificate, Cert2\<rbrace> \<in> set evs" |
1345 Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Certificate, Cert2\<rbrace> \<in> set evs" |
1346 apply (erule rev_mp) |
1346 apply (erule rev_mp) |
1347 apply (erule srb.induct) |
1347 apply (erule srb.induct) |
1348 prefer 18 apply (fastsimp dest: Outpts_A_Card_form_10) |
1348 prefer 18 apply (fastforce dest: Outpts_A_Card_form_10) |
1349 apply auto |
1349 apply auto |
1350 done |
1350 done |
1351 |
1351 |
1352 |
1352 |
1353 text{* step9integrity is @{term Inputs_A_Card_form_9} |
1353 text{* step9integrity is @{term Inputs_A_Card_form_9} |