author  bulwahn 
Wed, 11 Jul 2012 13:54:37 +0200  
changeset 48243  b149de01d669 
permissions  rwrr 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

1 
theory Needham_Schroeder_Unguided_Attacker_Example 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

2 
imports Needham_Schroeder_Base 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

3 
begin 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

4 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

5 
inductive_set ns_public :: "event list set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

6 
where 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

7 
(*Initial trace is empty*) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

8 
Nil: "[] \<in> ns_public" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

9 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

10 
 Fake: "\<lbrakk>evs1 \<in> ns_public; X \<in> synth (analz (spies evs1)) \<rbrakk> 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

11 
\<Longrightarrow> Says Spy A X # evs1 \<in> ns_public" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

12 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

13 
(*Alice initiates a protocol run, sending a nonce to Bob*) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

14 
 NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk> 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

15 
\<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

16 
# evs1 \<in> ns_public" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

17 
(*Bob responds to Alice's message with a further nonce*) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

18 
 NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2; 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

19 
Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk> 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

20 
\<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

21 
# evs2 \<in> ns_public" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

22 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

23 
(*Alice proves her existence by sending NB back to Bob.*) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

24 
 NS3: "\<lbrakk>evs3 \<in> ns_public; 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

25 
Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3; 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

26 
Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk> 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

27 
\<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

28 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

29 
declare ListMem_iff[symmetric, code_pred_inline] 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

30 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

31 
lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def] 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

32 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

33 
code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+ 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

34 
thm ns_publicp.equation 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

35 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

36 
code_pred [generator_cps] ns_publicp . 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

37 
thm ns_publicp.generator_cps_equation 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

38 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

39 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

40 
lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

41 
quickcheck[smart_exhaustive, depth = 5, timeout = 200, expect = counterexample] 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

42 
(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

43 
oops 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

44 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

45 
lemma 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

46 
"\<lbrakk>ns_publicp evs\<rbrakk> 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

47 
\<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

48 
\<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

49 
\<Longrightarrow> Nonce NB \<notin> analz (spies evs)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

50 
quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = no_counterexample] 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

51 
(*quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

52 
oops 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

53 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

54 
section {* Proving the counterexample trace for validation *} 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

55 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

56 
lemma 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

57 
assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

58 
assumes "evs = 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

59 
[Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)), 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

60 
Says Bob Alice (Crypt (pubEK Alice) {Nonce 0, Nonce 1}), 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

61 
Says Spy Bob (Crypt (pubEK Bob) {Nonce 0, Agent Alice}), 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

62 
Says Alice Spy (Crypt (pubEK Spy) {Nonce 0, Agent Alice})]" (is "_ = [?e3, ?e2, ?e1, ?e0]") 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

63 
shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

64 
proof  
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

65 
from assms show "A \<noteq> Spy" by auto 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

66 
from assms show "B \<noteq> Spy" by auto 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

67 
have "[] : ns_public" by (rule Nil) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

68 
then have first_step: "[?e0] : ns_public" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

69 
proof (rule NS1) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

70 
show "Nonce 0 ~: used []" by eval 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

71 
qed 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

72 
then have "[?e1, ?e0] : ns_public" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

73 
proof (rule Fake) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

74 
show "Crypt (pubEK Bob) {Nonce 0, Agent Alice} : synth (analz (knows Spy [?e0]))" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

75 
by (intro synth.intros(2,3,4,1)) eval+ 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

76 
qed 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

77 
then have "[?e2, ?e1, ?e0] : ns_public" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

78 
proof (rule NS2) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

79 
show "Says Spy Bob (Crypt (pubEK Bob) {Nonce 0, Agent Alice}) \<in> set [?e1, ?e0]" by simp 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

80 
show " Nonce 1 ~: used [?e1, ?e0]" by eval 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

81 
qed 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

82 
then show "evs : ns_public" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

83 
unfolding assms 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

84 
proof (rule NS3) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

85 
show " Says Alice Spy (Crypt (pubEK Spy) {Nonce 0, Agent Alice}) \<in> set [?e2, ?e1, ?e0]" by simp 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

86 
show "Says Bob Alice (Crypt (pubEK Alice) {Nonce 0, Nonce 1}) : set [?e2, ?e1, ?e0]" by simp 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

87 
qed 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

88 
from assms show "Nonce NB : analz (knows Spy evs)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

89 
apply simp 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

90 
apply (rule analz.intros(4)) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

91 
apply (rule analz.intros(1)) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

92 
apply (auto simp add: bad_def) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

93 
done 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

94 
qed 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

95 

b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

96 
end 