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

 \begin{isamarkuptext}%
 The system's behaviour is formalized as a set of traces of
 \emph{events}.  The most important event, \isa{Says\ A\ B\ X}, expresses
 $A\to B : X$, which is the attempt by~$A$ to send~$B$ the message~$X$.
 A trace is simply a list, constructed in reverse
-using~\isa{{\isacharhash}}.  Other event types include reception of messages (when
+using~\isa{{\isaliteral{23}{\isacharhash}}}.  Other event types include reception of messages (when
 we want to make it explicit) and an agent's storing a fact.
 
 Sometimes the protocol requires an agent to generate a new nonce. The
 probability that a 20-byte random number has appeared before is effectively
 zero.  To formalize this important property, the set \isa{used\ evs}
 denotes the set of all items mentioned in the trace~\isa{evs}.
 The function \isa{used} has a straightforward
 recursive definition.  Here is the case for \isa{Says} event:
 \begin{isabelle}%
-\ \ \ \ \ used\ {\isacharparenleft}Says\ A\ B\ X\ {\isacharhash}\ evs{\isacharparenright}\ {\isacharequal}\ parts\ {\isacharbraceleft}X{\isacharbraceright}\ {\isasymunion}\ used\ evs%
+\ \ \ \ \ used\ {\isaliteral{28}{\isacharparenleft}}Says\ A\ B\ X\ {\isaliteral{23}{\isacharhash}}\ evs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ parts\ {\isaliteral{7B}{\isacharbraceleft}}X{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ used\ evs%
 \end{isabelle}
 
 The function \isa{knows} formalizes an agent's knowledge.  Mostly we only
 care about the spy's knowledge, and \isa{knows\ Spy\ evs} is the set of items
 available to the spy in the trace~\isa{evs}.  Already in the empty trace,
 the spy starts with some secrets at his disposal, such as the private keys
 of compromised users.  After each \isa{Says} event, the spy learns the
 message that was sent:
 \begin{isabelle}%
-\ \ \ \ \ knows\ Spy\ {\isacharparenleft}Says\ A\ B\ X\ {\isacharhash}\ evs{\isacharparenright}\ {\isacharequal}\ insert\ X\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}%
+\ \ \ \ \ knows\ Spy\ {\isaliteral{28}{\isacharparenleft}}Says\ A\ B\ X\ {\isaliteral{23}{\isacharhash}}\ evs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ insert\ X\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}%
 \end{isabelle}
 Combinations of functions express other important
 sets of messages derived from~\isa{evs}:
 \begin{itemize}
-\item \isa{analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}} is everything that the spy could
+\item \isa{analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}} is everything that the spy could
 learn by decryption
-\item \isa{synth\ {\isacharparenleft}analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharparenright}} is everything that the spy
+\item \isa{synth\ {\isaliteral{28}{\isacharparenleft}}analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}} is everything that the spy
 could generate
 \end{itemize}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %