author  wenzelm 
Tue, 16 Jan 2018 09:58:17 +0100  
changeset 67445  4311845b0412 
parent 67399  eab6ce8368fa 
permissions  rwrr 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

1 
theory Needham_Schroeder_Guided_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_NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> 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 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

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

13 
 Fake_NS2: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<in> analz (spies evs1); Nonce NB \<in> analz (spies evs1) \<rbrakk> 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

14 
\<Longrightarrow> Says Spy 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

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

16 

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

17 
(*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

18 
 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

19 
\<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

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

21 
(*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

22 
 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

23 
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

24 
\<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

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

26 

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

27 
(*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

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

29 
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

30 
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

31 
\<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

32 

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

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

34 

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

35 
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

36 

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

37 
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

38 
thm ns_publicp.equation 
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 
code_pred [generator_cps] ns_publicp . 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

42 

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

43 

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

44 
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

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

46 
(*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

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

48 

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

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

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

51 
\<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

52 
\<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

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

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

55 
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

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

57 

62290  58 
section \<open>Proving the counterexample trace for validation\<close> 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

59 

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

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

61 
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

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

63 
[Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)), 
61984  64 
Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>), 
65 
Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>), 

66 
Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>)]" (is "_ = [?e3, ?e2, ?e1, ?e0]") 

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

67 
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

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

69 
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

70 
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

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

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

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

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

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

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

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

78 
show "Nonce 0 : analz (knows Spy [?e0])" by eval 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

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

81 
proof (rule NS2) 
61984  82 
show "Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e1, ?e0]" by simp 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

83 
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

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

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

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

87 
proof (rule NS3) 
61984  88 
show " Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e2, ?e1, ?e0]" by simp 
89 
show "Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>) 

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

90 
: set [?e2, ?e1, ?e0]" by simp 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

92 
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

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

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

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

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

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

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

99 

67399  100 
end 