\begin{figure}[h] \centering \begin{tikzpicture}[scale=0.155] \tikzstyle{every node}+=[inner sep=0pt] \draw [black] (8.6,-13) circle (4.7); \draw (8.6,-13) node {observe}; \draw [black] (26.9,-13) circle (4.7); \draw (26.9,-13) node {replay}; \draw [black] (46.1,-13) circle (4.7); \draw (46.1,-13) node {end}; \draw [black] (6.528,-8.802) arc (234:-54:3.525); \draw (8.6,-1.93) node [above, align=center] {\textit{copy} \texttt{msg} from \texttt{chan} to \texttt{buf} \\ \texttt{lim-=1}}; \fill [black] (10.67,-8.8) -- (11.55,-8.45) -- (10.74,-7.86); \draw [black] (10.672,-17.198) arc (54:-234:3.525); \draw (8.6,-24.08) node [below] {\textit{pass} \texttt{msg} on \texttt{chan}}; \fill [black] (6.53,-17.2) -- (5.65,-17.55) -- (6.46,-18.14); \draw [black] (0.2,-13) -- (3.9,-13); \fill [black] (3.9,-13) -- (3.1,-12.5) -- (3.1,-13.5); \draw [black] (31.6,-13) -- (41.4,-13); \fill [black] (41.4,-13) -- (40.6,-12.5) -- (40.6,-13.5); \draw (36.5,-12.5) node [above] {\texttt{buf} empty}; \draw [black] (13.3,-13) -- (22.2,-13); \fill [black] (22.2,-13) -- (21.4,-12.5) -- (21.4,-13.5); \draw (17.75,-12.5) node [above] {\texttt{lim=0}}; \draw [black] (28.972,-17.198) arc (54:-234:3.525); \draw (26.9,-24.08) node [below] {pass \texttt{msg} on \texttt{chan}}; \fill [black] (24.83,-17.2) -- (23.95,-17.55) -- (24.76,-18.14); \draw [black] (24.828,-8.802) arc (234:-54:3.525); \draw (26.9,-1.93) node [above] {\textit{send} \texttt{msg} from \texttt{buf} to \texttt{chan}}; \fill [black] (28.97,-8.8) -- (29.85,-8.45) -- (29.04,-7.86); \draw [black] (24.828,-8.802) arc (234:-54:3.525); \fill [black] (28.97,-8.8) -- (29.85,-8.45) -- (29.04,-7.86); \end{tikzpicture} \caption{High-level state machine diagram of the \textit{replay} attacker gadget, attacking a channel \texttt{chan}. A natural number \texttt{lim} is pre-defined. \texttt{buf} is a simple FIFO buffer of length \texttt{lim}.} \label{fig:replay} \end{figure}