doc-src/TutorialI/Protocol/document/Public.tex

 an abbreviation (cf.\ \S\ref{sec:abbreviations}) defined in terms of
 \isa{invKey} and \isa{pubK}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{consts}\isamarkupfalse%
-\ pubK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isasymRightarrow}\ key{\isachardoublequoteclose}\isanewline
+\ pubK\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}agent\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ key{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \isacommand{abbreviation}\isamarkupfalse%
-\ priK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isasymRightarrow}\ key{\isachardoublequoteclose}\isanewline
-\isakeyword{where}\ {\isachardoublequoteopen}priK\ x\ \ {\isasymequiv}\ \ invKey{\isacharparenleft}pubK\ x{\isacharparenright}{\isachardoublequoteclose}%
+\ priK\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}agent\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ key{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}priK\ x\ \ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ \ invKey{\isaliteral{28}{\isacharparenleft}}pubK\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
 \begin{isamarkuptext}%
 \noindent
 The set \isa{bad} consists of those agents whose private keys are known to
 the spy.
 

 any public key.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{axioms}\isamarkupfalse%
 \isanewline
-\ \ inj{\isacharunderscore}pubK{\isacharcolon}\ \ \ \ \ \ \ \ {\isachardoublequoteopen}inj\ pubK{\isachardoublequoteclose}\isanewline
-\ \ priK{\isacharunderscore}neq{\isacharunderscore}pubK{\isacharcolon}\ \ \ {\isachardoublequoteopen}priK\ A\ {\isasymnoteq}\ pubK\ B{\isachardoublequoteclose}%
+\ \ inj{\isaliteral{5F}{\isacharunderscore}}pubK{\isaliteral{3A}{\isacharcolon}}\ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}inj\ pubK{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ priK{\isaliteral{5F}{\isacharunderscore}}neq{\isaliteral{5F}{\isacharunderscore}}pubK{\isaliteral{3A}{\isacharcolon}}\ \ \ {\isaliteral{22}{\isachardoublequoteopen}}priK\ A\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ pubK\ B{\isaliteral{22}{\isachardoublequoteclose}}%
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof