author  traytel 
Mon, 24 Oct 2016 16:53:32 +0200  
changeset 64378  e9eb0b99a44c 
parent 62290  658276428cfc 
child 66453  cc19f7ca2ed6 
permissions  rwrr 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

2 
imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck" 
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 

58310  5 
datatype agent = Alice  Bob  Spy 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

6 

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

7 
definition agents :: "agent set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

9 
"agents = {Spy, Alice, Bob}" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

10 

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

11 
definition bad :: "agent set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

13 
"bad = {Spy}" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

14 

58310  15 
datatype key = pubEK agent  priEK agent 
48243
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 
fun invKey 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

19 
"invKey (pubEK A) = priEK A" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

20 
 "invKey (priEK A) = pubEK A" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

21 

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

23 
msg = Agent agent 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

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

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

27 
 Crypt key msg 
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 
syntax 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

30 
"_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

31 
translations 
61984  32 
"\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" 
33 
"\<lbrace>x, y\<rbrace>" == "CONST MPair x y" 

48243
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 
inductive_set 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

36 
parts :: "msg set => msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

37 
for H :: "msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

39 
Inj [intro]: "X \<in> H ==> X \<in> parts H" 
61984  40 
 Fst: "\<lbrace>X,Y\<rbrace> \<in> parts H ==> X \<in> parts H" 
41 
 Snd: "\<lbrace>X,Y\<rbrace> \<in> parts H ==> Y \<in> parts H" 

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

42 
 Body: "Crypt K X \<in> parts H ==> X \<in> parts H" 
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 
inductive_set 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

45 
analz :: "msg set => msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

46 
for H :: "msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

48 
Inj [intro,simp] : "X \<in> H ==> X \<in> analz H" 
61984  49 
 Fst: "\<lbrace>X,Y\<rbrace> \<in> analz H ==> X \<in> analz H" 
50 
 Snd: "\<lbrace>X,Y\<rbrace> \<in> analz H ==> Y \<in> analz H" 

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

51 
 Decrypt [dest]: 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

52 
"[Crypt K X \<in> analz H; Key(invKey K): analz H] ==> X \<in> analz H" 
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 
inductive_set 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

55 
synth :: "msg set => msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

56 
for H :: "msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

58 
Inj [intro]: "X \<in> H ==> X \<in> synth H" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

59 
 Agent [intro]: "Agent agt \<in> synth H" 
61984  60 
 MPair [intro]: "[X \<in> synth H; Y \<in> synth H] ==> \<lbrace>X,Y\<rbrace> \<in> synth H" 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

61 
 Crypt [intro]: "[X \<in> synth H; Key(K) \<in> H] ==> Crypt K X \<in> synth H" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

62 

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

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

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

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

66 
"initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

68 
"initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

70 
"initState Spy = (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

71 

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

73 
event = Says agent agent msg 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

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

76 

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

77 

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

78 
primrec knows :: "agent => event list => msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

80 
knows_Nil: "knows A [] = initState A" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

82 
"knows A (ev # evs) = 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

83 
(if A = Spy then 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

85 
Says A' B X => insert X (knows Spy evs) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

86 
 Gets A' X => knows Spy evs 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

87 
 Notes A' X => 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

88 
if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

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

91 
Says A' B X => 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

92 
if A'=A then insert X (knows A evs) else knows A evs 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

93 
 Gets A' X => 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

94 
if A'=A then insert X (knows A evs) else knows A evs 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

95 
 Notes A' X => 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

96 
if A'=A then insert X (knows A evs) else knows A evs))" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

97 

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

98 
abbreviation (input) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

99 
spies :: "event list => msg set" where 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

100 
"spies == knows Spy" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

101 

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

102 
primrec used :: "event list => msg set" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

103 
where 
61952  104 
used_Nil: "used [] = \<Union>(parts ` initState ` agents)" 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

105 
 used_Cons: "used (ev # evs) = 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

107 
Says A B X => parts {X} \<union> used evs 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

108 
 Gets A X => used evs 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

109 
 Notes A X => parts {X} \<union> used evs)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

110 

62290  111 
subsection \<open>Preparations for sets\<close> 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

112 

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

113 
fun find_first :: "('a => 'b option) => 'a list => 'b option" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

115 
"find_first f [] = None" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

116 
 "find_first f (x # xs) = (case f x of Some y => Some y  None => find_first f xs)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

117 

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

118 
consts cps_of_set :: "'a set => ('a => term list option) => term list option" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

119 

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

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

121 
[code]: "cps_of_set (set xs) f = find_first f xs" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

123 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
48618
diff
changeset

124 
consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => natural => (bool * term list) option" 
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
48618
diff
changeset

125 
consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued" 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

126 

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

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

128 
[code]: "pos_cps_of_set (set xs) f i = find_first f xs" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

130 

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

131 
consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

132 
=> 'b list => 'a Quickcheck_Exhaustive.three_valued" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

133 

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

134 
lemma [code]: 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

135 
"find_first' f [] = Quickcheck_Exhaustive.No_value" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

136 
"find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs  Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x  Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x  _ => Quickcheck_Exhaustive.Unknown_value))" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

138 

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

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

140 
[code]: "neg_cps_of_set (set xs) f i = find_first' f xs" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

142 

62290  143 
setup \<open> 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

145 
val Fun = Predicate_Compile_Aux.Fun 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

146 
val Input = Predicate_Compile_Aux.Input 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

147 
val Output = Predicate_Compile_Aux.Output 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

148 
val Bool = Predicate_Compile_Aux.Bool 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

149 
val oi = Fun (Output, Fun (Input, Bool)) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

150 
val ii = Fun (Input, Fun (Input, Bool)) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

151 
fun of_set compfuns (Type ("fun", [T, _])) = 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

152 
case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

153 
Type ("Quickcheck_Exhaustive.three_valued", _) => 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

154 
Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T > (Predicate_Compile_Aux.mk_monadT compfuns T)) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

155 
 Type ("Predicate.pred", _) => Const(@{const_name pred_of_set}, HOLogic.mk_setT T > Predicate_Compile_Aux.mk_monadT compfuns T) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

156 
 _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T > (Predicate_Compile_Aux.mk_monadT compfuns T)) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

157 
fun member compfuns (U as Type ("fun", [T, _])) = 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

158 
(absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

159 
(Const (@{const_name "Set.member"}, T > HOLogic.mk_setT T > @{typ bool}) $ Bound 1 $ Bound 0)))) 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

160 

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

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

162 
Core_Data.force_modes_and_compilations @{const_name Set.member} 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

163 
[(oi, (of_set, false)), (ii, (member, false))] 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

164 
end 
62290  165 
\<close> 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

166 

62290  167 
subsection \<open>Derived equations for analz, parts and synth\<close> 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

168 

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

169 
lemma [code]: 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

170 
"analz H = (let 
61984  171 
H' = H \<union> (\<Union>((%m. case m of \<lbrace>X, Y\<rbrace> => {X, Y}  Crypt K X => if Key (invKey K) : H then {X} else {}  _ => {}) ` H)) 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

172 
in if H' = H then H else analz H')" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

174 

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

175 
lemma [code]: 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

176 
"parts H = (let 
61984  177 
H' = H \<union> (\<Union>((%m. case m of \<lbrace>X, Y\<rbrace> => {X, Y}  Crypt K X => {X}  _ => {}) ` H)) 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

178 
in if H' = H then H else parts H')" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

180 

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

181 
definition synth' :: "msg set => msg => bool" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

183 
"synth' H m = (m : synth H)" 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

184 

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

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

186 

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

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

188 

62290  189 
setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}]\<close> 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

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

191 
declare [[quickcheck_timing]] 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

192 

58813  193 
setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation 
48243
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

194 
declare [[quickcheck_full_support = false]] 
b149de01d669
adding three variants of the NeedhamSchroeder formalisation as case studies for Quickcheck
bulwahn
parents:
diff
changeset

195 

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

196 
end 