diff -r 42671298f037 -r 313a24b66a8d doc-src/TutorialI/Protocol/document/Message.tex --- a/doc-src/TutorialI/Protocol/document/Message.tex Sun Nov 07 23:32:26 2010 +0100 +++ b/doc-src/TutorialI/Protocol/document/Message.tex Mon Nov 08 00:00:47 2010 +0100 @@ -41,16 +41,16 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{datatype}\isamarkupfalse% -\ agent\ {\isacharequal}\ Server\ {\isacharbar}\ Friend\ nat\ {\isacharbar}\ Spy% +\ agent\ {\isaliteral{3D}{\isacharequal}}\ Server\ {\isaliteral{7C}{\isacharbar}}\ Friend\ nat\ {\isaliteral{7C}{\isacharbar}}\ Spy% \begin{isamarkuptext}% Keys are just natural numbers. Function \isa{invKey} maps a public key to the matching private key, and vice versa:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{types}\isamarkupfalse% -\ key\ {\isacharequal}\ nat\isanewline +\ key\ {\isaliteral{3D}{\isacharequal}}\ nat\isanewline \isacommand{consts}\isamarkupfalse% -\ invKey\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}key\ {\isasymRightarrow}\ key{\isachardoublequoteclose}% +\ invKey\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}key\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ key{\isaliteral{22}{\isachardoublequoteclose}}% \isadelimproof % \endisadelimproof @@ -72,11 +72,11 @@ \isamarkuptrue% \isacommand{datatype}\isamarkupfalse% \isanewline -\ \ \ \ \ msg\ {\isacharequal}\ Agent\ \ agent\isanewline -\ \ \ \ \ \ \ \ \ {\isacharbar}\ Nonce\ \ nat\isanewline -\ \ \ \ \ \ \ \ \ {\isacharbar}\ Key\ \ \ \ key\isanewline -\ \ \ \ \ \ \ \ \ {\isacharbar}\ MPair\ \ msg\ msg\isanewline -\ \ \ \ \ \ \ \ \ {\isacharbar}\ Crypt\ \ key\ msg% +\ \ \ \ \ msg\ {\isaliteral{3D}{\isacharequal}}\ Agent\ \ agent\isanewline +\ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Nonce\ \ nat\isanewline +\ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Key\ \ \ \ key\isanewline +\ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ MPair\ \ msg\ msg\isanewline +\ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Crypt\ \ key\ msg% \begin{isamarkuptext}% \noindent The notation $\comp{X\sb 1,\ldots X\sb{n-1},X\sb n}$ @@ -85,7 +85,7 @@ Since datatype constructors are injective, we have the theorem \begin{isabelle}% -Crypt\ K\ X\ {\isacharequal}\ Crypt\ K{\isacharprime}\ X{\isacharprime}\ {\isasymLongrightarrow}\ K\ {\isacharequal}\ K{\isacharprime}\ {\isasymand}\ X\ {\isacharequal}\ X{\isacharprime}% +Crypt\ K\ X\ {\isaliteral{3D}{\isacharequal}}\ Crypt\ K{\isaliteral{27}{\isacharprime}}\ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ K\ {\isaliteral{3D}{\isacharequal}}\ K{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ X\ {\isaliteral{3D}{\isacharequal}}\ X{\isaliteral{27}{\isacharprime}}% \end{isabelle} A ciphertext can be decrypted using only one key and can yield only one plaintext. In the real world, decryption with the @@ -672,17 +672,17 @@ defined inductively.% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% \isanewline -\ \ analz\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}msg\ set\ {\isasymRightarrow}\ msg\ set{\isachardoublequoteclose}\isanewline -\ \ \isakeyword{for}\ H\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}msg\ set{\isachardoublequoteclose}\isanewline +\ \ analz\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}msg\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ msg\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isakeyword{for}\ H\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}msg\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline \ \ \isakeyword{where}\isanewline -\ \ \ \ Inj\ {\isacharbrackleft}intro{\isacharcomma}simp{\isacharbrackright}\ {\isacharcolon}\ {\isachardoublequoteopen}X\ {\isasymin}\ H\ {\isasymLongrightarrow}\ X\ {\isasymin}\ analz\ H{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ Fst{\isacharcolon}\ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrace}X{\isacharcomma}Y{\isasymrbrace}\ {\isasymin}\ analz\ H\ {\isasymLongrightarrow}\ X\ {\isasymin}\ analz\ H{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ Snd{\isacharcolon}\ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrace}X{\isacharcomma}Y{\isasymrbrace}\ {\isasymin}\ analz\ H\ {\isasymLongrightarrow}\ Y\ {\isasymin}\ analz\ H{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ Decrypt\ {\isacharbrackleft}dest{\isacharbrackright}{\isacharcolon}\ \isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}Crypt\ K\ X\ {\isasymin}\ analz\ H{\isacharsemicolon}\ Key{\isacharparenleft}invKey\ K{\isacharparenright}\ {\isasymin}\ analz\ H{\isasymrbrakk}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ X\ {\isasymin}\ analz\ H{\isachardoublequoteclose}% +\ \ \ \ Inj\ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{2C}{\isacharcomma}}simp{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ {\isaliteral{7C}{\isacharbar}}\ Fst{\isaliteral{3A}{\isacharcolon}}\ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}X{\isaliteral{2C}{\isacharcomma}}Y{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ {\isaliteral{7C}{\isacharbar}}\ Snd{\isaliteral{3A}{\isacharcolon}}\ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}X{\isaliteral{2C}{\isacharcomma}}Y{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ {\isaliteral{7C}{\isacharbar}}\ Decrypt\ {\isaliteral{5B}{\isacharbrackleft}}dest{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ \isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Crypt\ K\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H{\isaliteral{3B}{\isacharsemicolon}}\ Key{\isaliteral{28}{\isacharparenleft}}invKey\ K{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ analz\ H{\isaliteral{22}{\isachardoublequoteclose}}% \isadelimproof % \endisadelimproof @@ -1104,26 +1104,26 @@ message encrypted with key~$K$ if he has the matching key,~$K^{-1}$. Properties proved by rule induction include the following: \begin{isabelle}% -G\ {\isasymsubseteq}\ H\ {\isasymLongrightarrow}\ analz\ G\ {\isasymsubseteq}\ analz\ H\rulename{analz{\isacharunderscore}mono}\par\smallskip% -analz\ {\isacharparenleft}analz\ H{\isacharparenright}\ {\isacharequal}\ analz\ H\rulename{analz{\isacharunderscore}idem}% +G\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ analz\ G\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ analz\ H\rulename{analz{\isaliteral{5F}{\isacharunderscore}}mono}\par\smallskip% +analz\ {\isaliteral{28}{\isacharparenleft}}analz\ H{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ analz\ H\rulename{analz{\isaliteral{5F}{\isacharunderscore}}idem}% \end{isabelle} The set of fake messages that an intruder could invent -starting from~\isa{H} is \isa{synth{\isacharparenleft}analz\ H{\isacharparenright}}, where \isa{synth\ H} +starting from~\isa{H} is \isa{synth{\isaliteral{28}{\isacharparenleft}}analz\ H{\isaliteral{29}{\isacharparenright}}}, where \isa{synth\ H} formalizes what the adversary can build from the set of messages~$H$.% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% \isanewline -\ \ synth\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}msg\ set\ {\isasymRightarrow}\ msg\ set{\isachardoublequoteclose}\isanewline -\ \ \isakeyword{for}\ H\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}msg\ set{\isachardoublequoteclose}\isanewline +\ \ synth\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}msg\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ msg\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isakeyword{for}\ H\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}msg\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline \ \ \isakeyword{where}\isanewline -\ \ \ \ Inj\ \ \ \ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}X\ {\isasymin}\ H\ {\isasymLongrightarrow}\ X\ {\isasymin}\ synth\ H{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ Agent\ \ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}Agent\ agt\ {\isasymin}\ synth\ H{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ MPair\ \ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}X\ {\isasymin}\ synth\ H{\isacharsemicolon}\ \ Y\ {\isasymin}\ synth\ H{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymlbrace}X{\isacharcomma}Y{\isasymrbrace}\ {\isasymin}\ synth\ H{\isachardoublequoteclose}\isanewline -\ \ {\isacharbar}\ Crypt\ \ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}X\ {\isasymin}\ synth\ H{\isacharsemicolon}\ \ Key\ K\ {\isasymin}\ H{\isasymrbrakk}\ {\isasymLongrightarrow}\ Crypt\ K\ X\ {\isasymin}\ synth\ H{\isachardoublequoteclose}% +\ \ \ \ Inj\ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ {\isaliteral{7C}{\isacharbar}}\ Agent\ \ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Agent\ agt\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ {\isaliteral{7C}{\isacharbar}}\ MPair\ \ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{3B}{\isacharsemicolon}}\ \ Y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}X{\isaliteral{2C}{\isacharcomma}}Y{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ {\isaliteral{7C}{\isacharbar}}\ Crypt\ \ {\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{3B}{\isacharsemicolon}}\ \ Key\ K\ {\isaliteral{5C3C696E3E}{\isasymin}}\ H{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Crypt\ K\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{22}{\isachardoublequoteclose}}% \isadelimproof % \endisadelimproof @@ -1172,18 +1172,18 @@ Like \isa{analz}, this set operator is monotone and idempotent. It also satisfies an interesting equation involving \isa{analz}: \begin{isabelle}% -analz\ {\isacharparenleft}synth\ H{\isacharparenright}\ {\isacharequal}\ analz\ H\ {\isasymunion}\ synth\ H\rulename{analz{\isacharunderscore}synth}% +analz\ {\isaliteral{28}{\isacharparenleft}}synth\ H{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ analz\ H\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ synth\ H\rulename{analz{\isaliteral{5F}{\isacharunderscore}}synth}% \end{isabelle} Rule inversion plays a major role in reasoning about \isa{synth}, through declarations such as this one:% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{inductive{\isacharunderscore}cases}\isamarkupfalse% -\ Nonce{\isacharunderscore}synth\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}Nonce\ n\ {\isasymin}\ synth\ H{\isachardoublequoteclose}% +\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}\isamarkupfalse% +\ Nonce{\isaliteral{5F}{\isacharunderscore}}synth\ {\isaliteral{5B}{\isacharbrackleft}}elim{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Nonce\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H{\isaliteral{22}{\isachardoublequoteclose}}% \begin{isamarkuptext}% \noindent The resulting elimination rule replaces every assumption of the form -\isa{Nonce\ n\ {\isasymin}\ synth\ H} by \isa{Nonce\ n\ {\isasymin}\ H}, +\isa{Nonce\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ synth\ H} by \isa{Nonce\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ H}, expressing that a nonce cannot be guessed. A third operator, \isa{parts}, is useful for stating correctness @@ -1194,7 +1194,7 @@ Its definition resembles that of \isa{analz} except in the rule corresponding to the constructor \isa{Crypt}: \begin{isabelle}% -\ \ \ \ \ Crypt\ K\ X\ {\isasymin}\ parts\ H\ {\isasymLongrightarrow}\ X\ {\isasymin}\ parts\ H% +\ \ \ \ \ Crypt\ K\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts\ H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ X\ {\isaliteral{5C3C696E3E}{\isasymin}}\ parts\ H% \end{isabelle} The body of an encrypted message is always regarded as part of it. We can use \isa{parts} to express general well-formedness properties of a protocol,