author  bulwahn 
Tue, 10 Jul 2012 18:41:34 +0200  
changeset 48224  f2dd90cc724b 
child 48243  b149de01d669 
permissions  rwrr 
48224
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

1 
theory Needham_Schroeder_No_Attacker_Example 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

2 
imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

3 
begin 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

4 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

5 
datatype agent = Alice  Bob  Spy 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

6 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

7 
definition agents :: "agent set" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

8 
where 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

9 
"agents = {Spy, Alice, Bob}" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

10 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

11 
definition bad :: "agent set" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

12 
where 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

13 
"bad = {Spy}" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

14 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

15 
datatype key = pubEK agent  priEK agent 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

16 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

17 
fun invKey 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

18 
where 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

19 
"invKey (pubEK A) = priEK A" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

20 
 "invKey (priEK A) = pubEK A" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

21 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

22 
datatype 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

23 
msg = Agent agent {*Agent names*} 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

24 
 Key key 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

25 
 Nonce nat {*Unguessable nonces*} 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

26 
 MPair msg msg {*Compound messages*} 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

27 
 Crypt key msg {*Encryption, public or sharedkey*} 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

28 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

29 
text{*Concrete syntax: messages appear as {A,B,NA}, etc...*} 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

30 
syntax 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

31 
"_MTuple" :: "['a, args] => 'a * 'b" ("(2{_,/ _})") 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

32 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

33 
syntax (xsymbols) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

34 
"_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

35 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

36 
translations 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

37 
"{x, y, z}" == "{x, {y, z}}" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

38 
"{x, y}" == "CONST MPair x y" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

39 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

40 
inductive_set 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

41 
parts :: "msg set => msg set" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

42 
for H :: "msg set" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

43 
where 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

44 
Inj [intro]: "X \<in> H ==> X \<in> parts H" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

45 
 Fst: "{X,Y} \<in> parts H ==> X \<in> parts H" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

46 
 Snd: "{X,Y} \<in> parts H ==> Y \<in> parts H" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

47 
 Body: "Crypt K X \<in> parts H ==> X \<in> parts H" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

48 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

49 
inductive_set 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

50 
analz :: "msg set => msg set" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

51 
for H :: "msg set" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

52 
where 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

53 
Inj [intro,simp] : "X \<in> H ==> X \<in> analz H" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

54 
 Fst: "{X,Y} \<in> analz H ==> X \<in> analz H" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

55 
 Snd: "{X,Y} \<in> analz H ==> Y \<in> analz H" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

56 
 Decrypt [dest]: 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

57 
"[Crypt K X \<in> analz H; Key(invKey K): analz H] ==> X \<in> analz H" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

58 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

59 
inductive_set 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

60 
synth :: "msg set => msg set" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

61 
for H :: "msg set" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

62 
where 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

63 
Inj [intro]: "X \<in> H ==> X \<in> synth H" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

64 
 Agent [intro]: "Agent agt \<in> synth H" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

65 
 MPair [intro]: "[X \<in> synth H; Y \<in> synth H] ==> {X,Y} \<in> synth H" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

66 
 Crypt [intro]: "[X \<in> synth H; Key(K) \<in> H] ==> Crypt K X \<in> synth H" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

67 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

68 
primrec initState 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

69 
where 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

70 
initState_Alice: 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

71 
"initState Alice = {Key (priEK Alice)} \<union> (Key ` pubEK ` agents)" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

72 
 initState_Bob: 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

73 
"initState Bob = {Key (priEK Bob)} \<union> (Key ` pubEK ` agents)" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

74 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

75 
 initState_Spy: 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

76 
"initState Spy = (Key ` priEK ` bad) \<union> (Key ` pubEK ` agents)" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

77 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

78 
datatype 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

79 
event = Says agent agent msg 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

80 
 Gets agent msg 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

81 
 Notes agent msg 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

82 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

83 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

84 
primrec knows :: "agent => event list => msg set" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

85 
where 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

86 
knows_Nil: "knows A [] = initState A" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

87 
 knows_Cons: 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

88 
"knows A (ev # evs) = 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

89 
(if A = Spy then 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

90 
(case ev of 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

91 
Says A' B X => insert X (knows Spy evs) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

92 
 Gets A' X => knows Spy evs 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

93 
 Notes A' X => 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

94 
if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

95 
else 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

96 
(case ev of 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

97 
Says A' B X => 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

98 
if A'=A then insert X (knows A evs) else knows A evs 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

99 
 Gets A' X => 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

100 
if A'=A then insert X (knows A evs) else knows A evs 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

101 
 Notes A' X => 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

102 
if A'=A then insert X (knows A evs) else knows A evs))" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

103 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

104 
abbreviation (input) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

105 
spies :: "event list => msg set" where 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

106 
"spies == knows Spy" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

107 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

108 
primrec used :: "event list => msg set" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

109 
where 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

110 
used_Nil: "used [] = Union (parts ` initState ` agents)" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

111 
 used_Cons: "used (ev # evs) = 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

112 
(case ev of 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

113 
Says A B X => parts {X} \<union> used evs 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

114 
 Gets A X => used evs 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

115 
 Notes A X => parts {X} \<union> used evs)" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

116 
(* {*The case for @{term Gets} seems anomalous, but @{term Gets} always 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

117 
follows @{term Says} in real protocols. Seems difficult to change. 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

118 
See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}. *}*) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

119 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

120 
inductive_set ns_public :: "event list set" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

121 
where 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

122 
(*Initial trace is empty*) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

123 
Nil: "[] \<in> ns_public" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

124 
(*Alice initiates a protocol run, sending a nonce to Bob*) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

125 
 NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk> 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

126 
\<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

127 
# evs1 \<in> ns_public" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

128 
(*Bob responds to Alice's message with a further nonce*) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

129 
 NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2; 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

130 
Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk> 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

131 
\<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

132 
# evs2 \<in> ns_public" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

133 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

134 
(*Alice proves her existence by sending NB back to Bob.*) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

135 
 NS3: "\<lbrakk>evs3 \<in> ns_public; 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

136 
Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3; 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

137 
Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk> 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

138 
\<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

139 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

140 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

141 
subsection {* Preparations for sets *} 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

142 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

143 
fun find_first :: "('a => 'b option) => 'a list => 'b option" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

144 
where 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

145 
"find_first f [] = None" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

146 
 "find_first f (x # xs) = (case f x of Some y => Some y  None => find_first f xs)" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

147 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

148 
consts cps_of_set :: "'a set => ('a => term list option) => term list option" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

149 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

150 
lemma 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

151 
[code]: "cps_of_set (set xs) f = find_first f xs" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

152 
sorry 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

153 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

154 
consts pos_cps_of_set :: "'a set => ('a => (bool * term list) option) => code_numeral => (bool * term list) option" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

155 
consts neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => code_numeral => term list Quickcheck_Exhaustive.three_valued" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

156 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

157 
lemma 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

158 
[code]: "pos_cps_of_set (set xs) f i = find_first f xs" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

159 
sorry 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

160 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

161 
consts find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

162 
=> 'b list => 'a Quickcheck_Exhaustive.three_valued" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

163 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

164 
lemma [code]: 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

165 
"find_first' f [] = Quickcheck_Exhaustive.No_value" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

166 
"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))" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

167 
sorry 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

168 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

169 
lemma 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

170 
[code]: "neg_cps_of_set (set xs) f i = find_first' f xs" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

171 
sorry 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

172 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

173 
setup {* 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

174 
let 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

175 
val Fun = Predicate_Compile_Aux.Fun 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

176 
val Input = Predicate_Compile_Aux.Input 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

177 
val Output = Predicate_Compile_Aux.Output 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

178 
val Bool = Predicate_Compile_Aux.Bool 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

179 
val oi = Fun (Output, Fun (Input, Bool)) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

180 
val ii = Fun (Input, Fun (Input, Bool)) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

181 
fun of_set compfuns (Type ("fun", [T, _])) = 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

182 
case body_type (Predicate_Compile_Aux.mk_monadT compfuns T) of 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

183 
Type ("Quickcheck_Exhaustive.three_valued", _) => 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

184 
Const(@{const_name neg_cps_of_set}, HOLogic.mk_setT T > (Predicate_Compile_Aux.mk_monadT compfuns T)) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

185 
 Type ("Predicate.pred", _) => Const(@{const_name pred_of_set}, HOLogic.mk_setT T > Predicate_Compile_Aux.mk_monadT compfuns T) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

186 
 _ => Const(@{const_name pos_cps_of_set}, HOLogic.mk_setT T > (Predicate_Compile_Aux.mk_monadT compfuns T)) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

187 
fun member compfuns (U as Type ("fun", [T, _])) = 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

188 
(absdummy T (absdummy (HOLogic.mk_setT T) (Predicate_Compile_Aux.mk_if compfuns 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

189 
(Const (@{const_name "Set.member"}, T > HOLogic.mk_setT T > @{typ bool}) $ Bound 1 $ Bound 0)))) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

190 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

191 
in 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

192 
Core_Data.force_modes_and_compilations @{const_name Set.member} 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

193 
[(oi, (of_set, false)), (ii, (member, false))] 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

194 
end 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

195 
*} 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

196 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

197 
subsection {* Derived equations for analz, parts and synth *} 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

198 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

199 
lemma [code]: 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

200 
"analz H = (let 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

201 
H' = H \<union> (Union ((%m. case m of {X, Y} => {X, Y}  Crypt K X => if Key (invKey K) : H then {X} else {}  _ => {}) ` H)) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

202 
in if H' = H then H else analz H')" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

203 
sorry 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

204 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

205 
lemma [code]: 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

206 
"parts H = (let 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

207 
H' = H \<union> (Union ((%m. case m of {X, Y} => {X, Y}  Crypt K X => {X}  _ => {}) ` H)) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

208 
in if H' = H then H else parts H')" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

209 
sorry 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

210 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

211 
code_pred [skip_proof] ns_publicp . 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

212 
thm ns_publicp.equation 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

213 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

214 
code_pred [generator_cps] ns_publicp . 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

215 
thm ns_publicp.generator_cps_equation 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

216 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

217 
setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *} 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

218 
declare ListMem_iff[symmetric, code_pred_inline] 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

219 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

220 
declare [[quickcheck_timing]] 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

221 
setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *} 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

222 
declare [[quickcheck_full_support = false]] 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

223 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

224 
lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

225 
(*quickcheck[random, iterations = 1000000, size = 20, timeout = 3600, verbose] 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

226 
quickcheck[exhaustive, size = 8, timeout = 3600, verbose] 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

227 
quickcheck[narrowing, size = 7, timeout = 3600, verbose]*) 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

228 
quickcheck[smart_exhaustive, depth = 5, timeout = 30, expect = counterexample] 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

229 
oops 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

230 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

231 
lemma 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

232 
"\<lbrakk>ns_publicp evs\<rbrakk> 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

233 
\<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

234 
\<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

235 
\<Longrightarrow> Nonce NB \<notin> analz (spies evs)" 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

236 
quickcheck[smart_exhaustive, depth = 6, timeout = 30] 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

237 
quickcheck[narrowing, size = 6, timeout = 30, verbose] 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

238 
oops 
f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

239 

f2dd90cc724b
adding an example using Quickcheck to find a valid trace for the needhamschroeder protocol (a case study for Quickcheck)
bulwahn
parents:
diff
changeset

240 
end 