author  berghofe 
Mon, 23 Jul 2007 14:31:34 +0200  
changeset 23925  ee98c2528a8f 
child 27094  2cf13a72e170 
permissions  rwrr 
23925
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

1 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

2 
\begin{isabellebody}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

3 
\def\isabellecontext{NS{\isacharunderscore}Public}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

4 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

5 
\isadelimtheory 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

6 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

7 
\endisadelimtheory 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

8 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

9 
\isatagtheory 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

10 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

11 
\endisatagtheory 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

12 
{\isafoldtheory}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

13 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

14 
\isadelimtheory 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

15 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

16 
\endisadelimtheory 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

17 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

18 
\isamarkupsection{Modelling the Protocol \label{sec:modelling}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

19 
} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

20 
\isamarkuptrue% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

21 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

22 
\begin{figure} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

23 
\begin{isabelle} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

24 
\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

25 
\ ns{\isacharunderscore}public\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}event\ list\ set{\isachardoublequoteclose}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

26 
\ \ \isakeyword{where}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

27 
\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

28 
\ \ \ Nil{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ ns{\isacharunderscore}public{\isachardoublequoteclose}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

29 
\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

30 
\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

31 
\ {\isacharbar}\ Fake{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}evsf\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\ \ X\ {\isasymin}\ synth\ {\isacharparenleft}analz\ {\isacharparenleft}knows\ Spy\ evsf{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

32 
\ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ Says\ Spy\ B\ X\ \ {\isacharhash}\ evsf\ {\isasymin}\ ns{\isacharunderscore}public{\isachardoublequoteclose}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

33 
\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

34 
\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

35 
\ {\isacharbar}\ NS{\isadigit{1}}{\isacharcolon}\ \ {\isachardoublequoteopen}{\isasymlbrakk}evs{\isadigit{1}}\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\ \ Nonce\ NA\ {\isasymnotin}\ used\ evs{\isadigit{1}}{\isasymrbrakk}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

36 
\ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ Says\ A\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}{\isacharparenright}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

37 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharhash}\ evs{\isadigit{1}}\ \ {\isasymin}\ \ ns{\isacharunderscore}public{\isachardoublequoteclose}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

38 
\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

39 
\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

40 
\ {\isacharbar}\ NS{\isadigit{2}}{\isacharcolon}\ \ {\isachardoublequoteopen}{\isasymlbrakk}evs{\isadigit{2}}\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\ \ Nonce\ NB\ {\isasymnotin}\ used\ evs{\isadigit{2}}{\isacharsemicolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

41 
\ \ \ \ \ \ \ \ \ \ \ Says\ A{\isacharprime}\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}{\isacharparenright}\ {\isasymin}\ set\ evs{\isadigit{2}}{\isasymrbrakk}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

42 
\ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

43 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharhash}\ evs{\isadigit{2}}\ \ {\isasymin}\ \ ns{\isacharunderscore}public{\isachardoublequoteclose}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

44 
\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

45 
\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

46 
\ {\isacharbar}\ NS{\isadigit{3}}{\isacharcolon}\ \ {\isachardoublequoteopen}{\isasymlbrakk}evs{\isadigit{3}}\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

47 
\ \ \ \ \ \ \ \ \ \ \ Says\ A\ \ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}{\isacharparenright}\ {\isasymin}\ set\ evs{\isadigit{3}}{\isacharsemicolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

48 
\ \ \ \ \ \ \ \ \ \ \ Says\ B{\isacharprime}\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

49 
\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymin}\ set\ evs{\isadigit{3}}{\isasymrbrakk}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

50 
\ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ Says\ A\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isacharparenleft}Nonce\ NB{\isacharparenright}{\isacharparenright}\ {\isacharhash}\ evs{\isadigit{3}}\ {\isasymin}\ ns{\isacharunderscore}public{\isachardoublequoteclose}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

51 
\end{isabelle} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

52 
\caption{An Inductive Protocol Definition}\label{fig:ns_public} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

53 
\end{figure} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

54 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

55 
\begin{isamarkuptext}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

56 
Let us formalize the NeedhamSchroeder publickey protocol, as corrected by 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

57 
Lowe: 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

58 
\begin{alignat*% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

59 
}{2} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

60 
&1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

61 
&2.&\quad B\to A &: \comp{Na,Nb,B}\sb{Ka} \\ 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

62 
&3.&\quad A\to B &: \comp{Nb}\sb{Kb} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

63 
\end{alignat*% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

64 
} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

65 

ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

66 
Each protocol step is specified by a rule of an inductive definition. An 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

67 
event trace has type \isa{event\ list}, so we declare the constant 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

68 
\isa{ns{\isacharunderscore}public} to be a set of such traces. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

69 

ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

70 
Figure~\ref{fig:ns_public} presents the inductive definition. The 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

71 
\isa{Nil} rule introduces the empty trace. The \isa{Fake} rule models the 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

72 
adversary's sending a message built from components taken from past 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

73 
traffic, expressed using the functions \isa{synth} and 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

74 
\isa{analz}. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

75 
The next three rules model how honest agents would perform the three 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

76 
protocol steps. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

77 

ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

78 
Here is a detailed explanation of rule \isa{NS{\isadigit{2}}}. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

79 
A trace containing an event of the form 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

80 
\begin{isabelle}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

81 
\ \ \ \ \ Says\ A{\isacharprime}\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}{\isacharparenright}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

82 
\end{isabelle} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

83 
may be extended by an event of the form 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

84 
\begin{isabelle}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

85 
\ \ \ \ \ Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

86 
\end{isabelle} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

87 
where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymin}\ used\ evs{\isadigit{2}}}. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

88 
Writing the sender as \isa{A{\isacharprime}} indicates that \isa{B} does not 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

89 
know who sent the message. Calling the trace variable \isa{evs{\isadigit{2}}} rather 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

90 
than simply \isa{evs} helps us know where we are in a proof after many 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

91 
casesplits: every subgoal mentioning \isa{evs{\isadigit{2}}} involves message~2 of the 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

92 
protocol. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

93 

ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

94 
Benefits of this approach are simplicity and clarity. The semantic model 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

95 
is set theory, proofs are by induction and the translation from the informal 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

96 
notation to the inductive rules is straightforward.% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

97 
\end{isamarkuptext}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

98 
\isamarkuptrue% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

99 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

100 
\isamarkupsection{Proving Elementary Properties \label{sec:regularity}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

101 
} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

102 
\isamarkuptrue% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

103 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

104 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

105 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

106 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

107 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

108 
\isatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

109 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

110 
\endisatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

111 
{\isafoldproof}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

112 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

113 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

114 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

115 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

116 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

117 
\begin{isamarkuptext}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

118 
Secrecy properties can be hard to prove. The conclusion of a typical 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

119 
secrecy theorem is 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

120 
\isa{X\ {\isasymnotin}\ analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}}. The difficulty arises from 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

121 
having to reason about \isa{analz}, or less formally, showing that the spy 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

122 
can never learn~\isa{X}. Much easier is to prove that \isa{X} can never 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

123 
occur at all. Such \emph{regularity} properties are typically expressed 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

124 
using \isa{parts} rather than \isa{analz}. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

125 

ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

126 
The following lemma states that \isa{A}'s private key is potentially 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

127 
known to the spy if and only if \isa{A} belongs to the set \isa{bad} of 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

128 
compromised agents. The statement uses \isa{parts}: the very presence of 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

129 
\isa{A}'s private key in a message, whether protected by encryption or 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

130 
not, is enough to confirm that \isa{A} is compromised. The proof, like 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

131 
nearly all protocol proofs, is by induction over traces.% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

132 
\end{isamarkuptext}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

133 
\isamarkuptrue% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

134 
\isacommand{lemma}\isamarkupfalse% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

135 
\ Spy{\isacharunderscore}see{\isacharunderscore}priK\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

136 
\ \ \ \ \ \ {\isachardoublequoteopen}evs\ {\isasymin}\ ns{\isacharunderscore}public\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

137 
\ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Key\ {\isacharparenleft}priK\ A{\isacharparenright}\ {\isasymin}\ parts\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}A\ {\isasymin}\ bad{\isacharparenright}{\isachardoublequoteclose}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

138 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

139 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

140 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

141 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

142 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

143 
\isatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

144 
\isacommand{apply}\isamarkupfalse% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

145 
\ {\isacharparenleft}erule\ ns{\isacharunderscore}public{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

146 
\begin{isamarkuptxt}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

147 
The induction yields five subgoals, one for each rule in the definition of 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

148 
\isa{ns{\isacharunderscore}public}. The idea is to prove that the protocol property holds initially 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

149 
(rule \isa{Nil}), is preserved by each of the legitimate protocol steps (rules 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

150 
\isa{NS{\isadigit{1}}}\isa{{\isadigit{3}}}), and even is preserved in the face of anything the 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

151 
spy can do (rule \isa{Fake}). 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

152 

ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

153 
The proof is trivial. No legitimate protocol rule sends any keys 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

154 
at all, so only \isa{Fake} is relevant. Indeed, simplification leaves 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

155 
only the \isa{Fake} case, as indicated by the variable name \isa{evsf}: 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

156 
\begin{isabelle}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

157 
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}evsf\ X{\isachardot}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

158 
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}evsf\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

159 
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }{\isacharparenleft}Key\ {\isacharparenleft}priK\ A{\isacharparenright}\ {\isasymin}\ parts\ {\isacharparenleft}knows\ Spy\ evsf{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}A\ {\isasymin}\ bad{\isacharparenright}{\isacharsemicolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

160 
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }X\ {\isasymin}\ synth\ {\isacharparenleft}analz\ {\isacharparenleft}knows\ Spy\ evsf{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

161 
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}Key\ {\isacharparenleft}priK\ A{\isacharparenright}\ {\isasymin}\ parts\ {\isacharparenleft}insert\ X\ {\isacharparenleft}knows\ Spy\ evsf{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

162 
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }{\isacharparenleft}A\ {\isasymin}\ bad{\isacharparenright}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

163 
\end{isabelle}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

164 
\end{isamarkuptxt}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

165 
\isamarkuptrue% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

166 
\isacommand{by}\isamarkupfalse% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

167 
\ blast% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

168 
\endisatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

169 
{\isafoldproof}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

170 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

171 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

172 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

173 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

174 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

175 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

176 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

177 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

178 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

179 
\isatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

180 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

181 
\endisatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

182 
{\isafoldproof}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

183 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

184 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

185 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

186 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

187 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

188 
\begin{isamarkuptext}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

189 
The \isa{Fake} case is proved automatically. If 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

190 
\isa{priK\ A} is in the extended trace then either (1) it was already in the 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

191 
original trace or (2) it was 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

192 
generated by the spy, who must have known this key already. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

193 
Either way, the induction hypothesis applies. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

194 

ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

195 
\emph{Unicity} lemmas are regularity lemmas stating that specified items 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

196 
can occur only once in a trace. The following lemma states that a nonce 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

197 
cannot be used both as $Na$ and as $Nb$ unless 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

198 
it is known to the spy. Intuitively, it holds because honest agents 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

199 
always choose fresh values as nonces; only the spy might reuse a value, 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

200 
and he doesn't know this particular value. The proof script is short: 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

201 
induction, simplification, \isa{blast}. The first line uses the rule 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

202 
\isa{rev{\isacharunderscore}mp} to prepare the induction by moving two assumptions into the 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

203 
induction formula.% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

204 
\end{isamarkuptext}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

205 
\isamarkuptrue% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

206 
\isacommand{lemma}\isamarkupfalse% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

207 
\ no{\isacharunderscore}nonce{\isacharunderscore}NS{\isadigit{1}}{\isacharunderscore}NS{\isadigit{2}}{\isacharcolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

208 
\ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}Crypt\ {\isacharparenleft}pubK\ C{\isacharparenright}\ {\isasymlbrace}NA{\isacharprime}{\isacharcomma}\ Nonce\ NA{\isacharcomma}\ Agent\ D{\isasymrbrace}\ {\isasymin}\ parts\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharsemicolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

209 
\ \ \ \ \ \ Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}\ {\isasymin}\ parts\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharsemicolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

210 
\ \ \ \ \ \ evs\ {\isasymin}\ ns{\isacharunderscore}public{\isasymrbrakk}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

211 
\ \ \ \ \ {\isasymLongrightarrow}\ Nonce\ NA\ {\isasymin}\ analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isachardoublequoteclose}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

212 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

213 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

214 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

215 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

216 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

217 
\isatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

218 
\isacommand{apply}\isamarkupfalse% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

219 
\ {\isacharparenleft}erule\ rev{\isacharunderscore}mp{\isacharcomma}\ erule\ rev{\isacharunderscore}mp{\isacharparenright}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

220 
\isacommand{apply}\isamarkupfalse% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

221 
\ {\isacharparenleft}erule\ ns{\isacharunderscore}public{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

222 
\isacommand{apply}\isamarkupfalse% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

223 
\ {\isacharparenleft}blast\ intro{\isacharcolon}\ analz{\isacharunderscore}insertI{\isacharparenright}{\isacharplus}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

224 
\isacommand{done}\isamarkupfalse% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

225 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

226 
\endisatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

227 
{\isafoldproof}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

228 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

229 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

230 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

231 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

232 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

233 
\begin{isamarkuptext}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

234 
The following unicity lemma states that, if \isa{NA} is secret, then its 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

235 
appearance in any instance of message~1 determines the other components. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

236 
The proof is similar to the previous one.% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

237 
\end{isamarkuptext}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

238 
\isamarkuptrue% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

239 
\isacommand{lemma}\isamarkupfalse% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

240 
\ unique{\isacharunderscore}NA{\isacharcolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

241 
\ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}Crypt{\isacharparenleft}pubK\ B{\isacharparenright}\ \ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A\ {\isasymrbrace}\ {\isasymin}\ parts{\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharsemicolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

242 
\ \ \ \ \ \ \ Crypt{\isacharparenleft}pubK\ B{\isacharprime}{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isacharprime}{\isasymrbrace}\ {\isasymin}\ parts{\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharsemicolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

243 
\ \ \ \ \ \ \ Nonce\ NA\ {\isasymnotin}\ analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharsemicolon}\ evs\ {\isasymin}\ ns{\isacharunderscore}public{\isasymrbrakk}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

244 
\ \ \ \ \ \ {\isasymLongrightarrow}\ A{\isacharequal}A{\isacharprime}\ {\isasymand}\ B{\isacharequal}B{\isacharprime}{\isachardoublequoteclose}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

245 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

246 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

247 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

248 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

249 
\isatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

250 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

251 
\endisatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

252 
{\isafoldproof}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

253 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

254 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

255 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

256 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

257 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

258 
\isamarkupsection{Proving Secrecy Theorems \label{sec:secrecy}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

259 
} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

260 
\isamarkuptrue% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

261 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

262 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

263 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

264 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

265 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

266 
\isatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

267 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

268 
\endisatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

269 
{\isafoldproof}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

270 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

271 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

272 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

273 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

274 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

275 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

276 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

277 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

278 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

279 
\isatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

280 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

281 
\endisatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

282 
{\isafoldproof}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

283 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

284 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

285 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

286 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

287 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

288 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

289 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

290 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

291 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

292 
\isatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

293 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

294 
\endisatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

295 
{\isafoldproof}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

296 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

297 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

298 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

299 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

300 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

301 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

302 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

303 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

304 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

305 
\isatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

306 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

307 
\endisatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

308 
{\isafoldproof}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

309 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

310 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

311 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

312 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

313 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

314 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

315 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

316 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

317 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

318 
\isatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

319 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

320 
\endisatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

321 
{\isafoldproof}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

322 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

323 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

324 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

325 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

326 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

327 
\begin{isamarkuptext}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

328 
The secrecy theorems for Bob (the second participant) are especially 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

329 
important because they fail for the original protocol. The following 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

330 
theorem states that if Bob sends message~2 to Alice, and both agents are 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

331 
uncompromised, then Bob's nonce will never reach the spy.% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

332 
\end{isamarkuptext}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

333 
\isamarkuptrue% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

334 
\isacommand{theorem}\isamarkupfalse% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

335 
\ Spy{\isacharunderscore}not{\isacharunderscore}see{\isacharunderscore}NB\ {\isacharbrackleft}dest{\isacharbrackright}{\isacharcolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

336 
\ {\isachardoublequoteopen}{\isasymlbrakk}Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\ {\isasymin}\ set\ evs{\isacharsemicolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

337 
\ \ \ A\ {\isasymnotin}\ bad{\isacharsemicolon}\ \ B\ {\isasymnotin}\ bad{\isacharsemicolon}\ \ evs\ {\isasymin}\ ns{\isacharunderscore}public{\isasymrbrakk}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

338 
\ \ {\isasymLongrightarrow}\ Nonce\ NB\ {\isasymnotin}\ analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isachardoublequoteclose}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

339 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

340 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

341 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

342 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

343 
\isatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

344 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

345 
\begin{isamarkuptxt}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

346 
To prove it, we must formulate the induction properly (one of the 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

347 
assumptions mentions~\isa{evs}), apply induction, and simplify:% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

348 
\end{isamarkuptxt}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

349 
\isamarkuptrue% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

350 
\isacommand{apply}\isamarkupfalse% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

351 
\ {\isacharparenleft}erule\ rev{\isacharunderscore}mp{\isacharcomma}\ erule\ ns{\isacharunderscore}public{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

352 
\begin{isamarkuptxt}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

353 
The proof states are too complicated to present in full. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

354 
Let's examine the simplest subgoal, that for message~1. The following 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

355 
event has just occurred: 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

356 
\[ 1.\quad A'\to B' : \comp{Na',A'}\sb{Kb'} \] 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

357 
The variables above have been primed because this step 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

358 
belongs to a different run from that referred to in the theorem 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

359 
statement  the theorem 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

360 
refers to a past instance of message~2, while this subgoal 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

361 
concerns message~1 being sent just now. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

362 
In the Isabelle subgoal, instead of primed variables like $B'$ and $Na'$ 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

363 
we have \isa{Ba} and~\isa{NAa}: 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

364 
\begin{isabelle}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

365 
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}evs{\isadigit{1}}\ NAa\ Ba{\isachardot}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

366 
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}A\ {\isasymnotin}\ bad{\isacharsemicolon}\ B\ {\isasymnotin}\ bad{\isacharsemicolon}\ evs{\isadigit{1}}\ {\isasymin}\ ns{\isacharunderscore}public{\isacharsemicolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

367 
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

368 
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }{\isasymin}\ set\ evs{\isadigit{1}}\ {\isasymlongrightarrow}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

369 
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }Nonce\ NB\ {\isasymnotin}\ analz\ {\isacharparenleft}knows\ Spy\ evs{\isadigit{1}}{\isacharparenright}{\isacharsemicolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

370 
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }Nonce\ NAa\ {\isasymnotin}\ used\ evs{\isadigit{1}}{\isasymrbrakk}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

371 
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Ba\ {\isasymin}\ bad\ {\isasymlongrightarrow}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

372 
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

373 
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }{\isasymin}\ set\ evs{\isadigit{1}}\ {\isasymlongrightarrow}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

374 
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }NB\ {\isasymnoteq}\ NAa% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

375 
\end{isabelle} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

376 
The simplifier has used a 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

377 
default simplification rule that does a case 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

378 
analysis for each encrypted message on whether or not the decryption key 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

379 
is compromised. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

380 
\begin{isabelle}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

381 
analz\ {\isacharparenleft}insert\ {\isacharparenleft}Crypt\ K\ X{\isacharparenright}\ H{\isacharparenright}\ {\isacharequal}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

382 
{\isacharparenleft}if\ Key\ {\isacharparenleft}invKey\ K{\isacharparenright}\ {\isasymin}\ analz\ H\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

383 
\isaindent{{\isacharparenleft}}then\ insert\ {\isacharparenleft}Crypt\ K\ X{\isacharparenright}\ {\isacharparenleft}analz\ {\isacharparenleft}insert\ X\ H{\isacharparenright}{\isacharparenright}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

384 
\isaindent{{\isacharparenleft}}else\ insert\ {\isacharparenleft}Crypt\ K\ X{\isacharparenright}\ {\isacharparenleft}analz\ H{\isacharparenright}{\isacharparenright}\rulename{analz{\isacharunderscore}Crypt{\isacharunderscore}if}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

385 
\end{isabelle} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

386 
The simplifier has also used \isa{Spy{\isacharunderscore}see{\isacharunderscore}priK}, proved in 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

387 
{\S}\ref{sec:regularity}) above, to yield \isa{Ba\ {\isasymin}\ bad}. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

388 

ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

389 
Recall that this subgoal concerns the case 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

390 
where the last message to be sent was 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

391 
\[ 1.\quad A'\to B' : \comp{Na',A'}\sb{Kb'}. \] 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

392 
This message can compromise $Nb$ only if $Nb=Na'$ and $B'$ is compromised, 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

393 
allowing the spy to decrypt the message. The Isabelle subgoal says 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

394 
precisely this, if we allow for its choice of variable names. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

395 
Proving \isa{NB\ {\isasymnoteq}\ NAa} is easy: \isa{NB} was 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

396 
sent earlier, while \isa{NAa} is fresh; formally, we have 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

397 
the assumption \isa{Nonce\ NAa\ {\isasymnotin}\ used\ evs{\isadigit{1}}}. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

398 

ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

399 
Note that our reasoning concerned \isa{B}'s participation in another 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

400 
run. Agents may engage in several runs concurrently, and some attacks work 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

401 
by interleaving the messages of two runs. With model checking, this 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

402 
possibility can cause a statespace explosion, and for us it 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

403 
certainly complicates proofs. The biggest subgoal concerns message~2. It 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

404 
splits into several cases, such as whether or not the message just sent is 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

405 
the very message mentioned in the theorem statement. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

406 
Some of the cases are proved by unicity, others by 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

407 
the induction hypothesis. For all those complications, the proofs are 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

408 
automatic by \isa{blast} with the theorem \isa{no{\isacharunderscore}nonce{\isacharunderscore}NS{\isadigit{1}}{\isacharunderscore}NS{\isadigit{2}}}. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

409 

ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

410 
The remaining theorems about the protocol are not hard to prove. The 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

411 
following one asserts a form of \emph{authenticity}: if 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

412 
\isa{B} has sent an instance of message~2 to~\isa{A} and has received the 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

413 
expected reply, then that reply really originated with~\isa{A}. The 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

414 
proof is a simple induction.% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

415 
\end{isamarkuptxt}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

416 
\isamarkuptrue% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

417 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

418 
\endisatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

419 
{\isafoldproof}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

420 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

421 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

422 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

423 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

424 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

425 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

426 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

427 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

428 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

429 
\isatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

430 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

431 
\endisatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

432 
{\isafoldproof}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

433 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

434 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

435 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

436 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

437 
\isacommand{theorem}\isamarkupfalse% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

438 
\ B{\isacharunderscore}trusts{\isacharunderscore}NS{\isadigit{3}}{\isacharcolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

439 
\ {\isachardoublequoteopen}{\isasymlbrakk}Says\ B\ A\ \ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}\ {\isasymin}\ set\ evs{\isacharsemicolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

440 
\ \ \ Says\ A{\isacharprime}\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isacharparenleft}Nonce\ NB{\isacharparenright}{\isacharparenright}\ {\isasymin}\ set\ evs{\isacharsemicolon}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

441 
\ \ \ A\ {\isasymnotin}\ bad{\isacharsemicolon}\ \ B\ {\isasymnotin}\ bad{\isacharsemicolon}\ \ evs\ {\isasymin}\ ns{\isacharunderscore}public{\isasymrbrakk}\isanewline 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

442 
\ \ {\isasymLongrightarrow}\ Says\ A\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isacharparenleft}Nonce\ NB{\isacharparenright}{\isacharparenright}\ {\isasymin}\ set\ evs{\isachardoublequoteclose}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

443 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

444 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

445 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

446 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

447 
\isatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

448 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

449 
\endisatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

450 
{\isafoldproof}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

451 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

452 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

453 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

454 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

455 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

456 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

457 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

458 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

459 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

460 
\isatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

461 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

462 
\endisatagproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

463 
{\isafoldproof}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

464 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

465 
\isadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

466 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

467 
\endisadelimproof 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

468 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

469 
\begin{isamarkuptext}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

470 
From similar assumptions, we can prove that \isa{A} started the protocol 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

471 
run by sending an instance of message~1 involving the nonce~\isa{NA}\@. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

472 
For this theorem, the conclusion is 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

473 
\begin{isabelle}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

474 
Says\ A\ B\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ B{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Agent\ A{\isasymrbrace}{\isacharparenright}\ {\isasymin}\ set\ evs% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

475 
\end{isabelle} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

476 
Analogous theorems can be proved for~\isa{A}, stating that nonce~\isa{NA} 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

477 
remains secret and that message~2 really originates with~\isa{B}. Even the 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

478 
flawed protocol establishes these properties for~\isa{A}; 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

479 
the flaw only harms the second participant. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

480 

ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

481 
\medskip 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

482 

ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

483 
Detailed information on this protocol verification technique can be found 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

484 
elsewhere~\cite{paulsonjcs}, including proofs of an Internet 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

485 
protocol~\cite{paulsontls}. We must stress that the protocol discussed 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

486 
in this chapter is trivial. There are only three messages; no keys are 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

487 
exchanged; we merely have to prove that encrypted data remains secret. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

488 
Real world protocols are much longer and distribute many secrets to their 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

489 
participants. To be realistic, the model has to include the possibility 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

490 
of keys being lost dynamically due to carelessness. If those keys have 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

491 
been used to encrypt other sensitive information, there may be cascading 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

492 
losses. We may still be able to establish a bound on the losses and to 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

493 
prove that other protocol runs function 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

494 
correctly~\cite{paulsonyahalom}. Proofs of realworld protocols follow 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

495 
the strategy illustrated above, but the subgoals can 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

496 
be much bigger and there are more of them. 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

497 
\index{protocols!security)}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

498 
\end{isamarkuptext}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

499 
\isamarkuptrue% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

500 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

501 
\isadelimtheory 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

502 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

503 
\endisadelimtheory 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

504 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

505 
\isatagtheory 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

506 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

507 
\endisatagtheory 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

508 
{\isafoldtheory}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

509 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

510 
\isadelimtheory 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

511 
% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

512 
\endisadelimtheory 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

513 
\end{isabellebody}% 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

514 
%%% Local Variables: 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

515 
%%% mode: latex 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

516 
%%% TeXmaster: "root" 
ee98c2528a8f
LaTeX code is now generated directly from theory files.
berghofe
parents:
diff
changeset

517 
%%% End: 