\def\lbb{\mathopen{\{\kern-.25em|}}
\def\rbb{\mathclose{|\kern-.25em\}}}
\def\comp#1{\lbb#1\rbb}
\newcommand\ins{\mathop{\mathsf{ins}}}
\newcommand\INS[1]{\{#1\}\cup}

\newcommand\Server{\mathop{\mathsf{Server}}}
\newcommand\server{\mathsf{S}}
\newcommand\Friend{\mathop{\mathsf{Friend}}}
\newcommand\Spy{\mathsf{Spy}}
\newcommand\kas{\mathop{\mathsf{Kas}}}
\newcommand\tgs{\mathop{\mathsf{Tgs}}}
\newcommand\sr{\mathop{\mathsf{SR}}}

\newcommand\Agent{\mathop{\mathsf{Agent}}}
\newcommand\Nonce{\mathop{\mathsf{Nonce}}}
\newcommand\Number{\mathop{\mathsf{Number}}}
\newcommand\Ct{\mathop{\mathsf{ct}}}
\newcommand\Na{\mathit{Na}}
\newcommand\Ca{\mathit{C_a}}
\newcommand\Cb{\mathit{C_b}}
\newcommand\Cp{\mathit{C_p}}
\newcommand\Nb{\mathit{Nb}}
\newcommand\Pk{\mathit{Pk}}
\newcommand\Nc{\mathit{Nc}}
\newcommand\Nx{\mathit{Nx}}
\newcommand\Np{\mathit{Np}}
\newcommand\ak{\mathit{authK}}
\newcommand\aks{\mathsf{AuthKeys}}
\newcommand\at{\mathit{authTicket}}
\newcommand\sk{\mathit{servK}}
\newcommand\st{\mathit{servTicket}}
\newcommand\Tt{\mathit{Ts}}
\newcommand\Tuno{\mathit{T_1}}
\newcommand\Tdue{\mathit{T_2}}
\newcommand\Ttre{\mathit{T_3}}
\newcommand\Ta{\mathit{Ta}}
\newcommand\Ts{\mathit{Ts}}
\newcommand\Tk{\mathit{Tk}}
\newcommand\ticket{\mathit{ticket}}
\newcommand\authenticatoruno{\mathit{authenticator1}}
\newcommand\authenticatordue{\mathit{authenticator2}}
\newcommand\authenticatortre{\mathit{authenticator3}}
\newcommand\Tx{\mathit{Tx}}
\newcommand\Key{\mathop{\mathsf{Key}}}
\newcommand\Ka{\mathit{Ka}}
\newcommand\Kb{\mathit{Kb}}
\newcommand\Kp{\mathit{Kp}}
\newcommand\Ktgs{\mathit{Ktgs}}
\newcommand\Kc{\mathit{Kc}}
\newcommand\Kd{\mathit{Kd}}
\newcommand\Kx{\mathit{Kx}}
\newcommand\Ks{\mathit{K}\mathsf{s}}
\newcommand\Kab{\mathit{Kab}}
\newcommand\Kcd{\mathit{Kcd}}
\newcommand\Kca{\mathit{Kca}}
\newcommand\PKab{\mathit{\Pi_{ab}}}
\newcommand\pkab{\mathit{\pi_{ab}}}
\newcommand\KCa{\mathit{K_{Ca}}}
\newcommand\KCp{\mathit{K_{Cp}}}
\newcommand\Hash{\mathop{\mathsf{Hash}}\nolimits}
\newcommand\Crypt{\mathop{\mathsf{Crypt}}}
\newcommand\parts{\mathop{\mathsf{parts}}}
\newcommand\analz{\mathop{\mathsf{analz}}}
\newcommand\synth{\mathop{\mathsf{synth}}}
\newcommand\tl{\mathop{\mathsf{tl}}}
\newcommand\keysFor{\mathop{\mathsf{keysFor}}}
\newcommand\traces{\mathop{\mathsf{traces}}}
\newcommand\bad{\mathop{\mathsf{bad}}}
%\newcommand\range{\mathop{\mathsf{range}}}

\newcommand\ea[2]{\mathsf{expiredAK}\,#1\,#2}
\newcommand\es[2]{\mathsf{expiredSK}\,#1\,#2}
\newcommand\kck[3]{\mathsf{AKcryptSK}\,#1\,#2\,#3}
\newcommand\SAYS{\mathop{\mathsf{Says}}}
\newcommand\Says[3]{\mathsf{Says}\,#1\,#2\,#3}
\newcommand\In[3]{\mathsf{Inputs}\,#1\,#2\,#3}
\newcommand\Out[3]{\mathsf{Outputs}\,#1\,#2\,#3}
\newcommand\out{\mathsf{Outputs}}
\newcommand\inp{\mathsf{Inputs}}
\newcommand\Notes[2]{\mathsf{Notes}\,#1\,#2}
\newcommand\Gets[2]{\mathsf{Gets}\,#1\,#2}
\newcommand\C{\mathsf{Gets\_c}}
\newcommand\A{\mathsf{Gets\_a}}
\newcommand\CGets[2]{\mathsf{Gets\_c}\,#1\,#2}
\newcommand\AGets[2]{\mathsf{Gets\_a}\,#1\,#2}
\newcommand\spies[1]{\mathsf{spies}\,#1}
\newcommand\knows[2]{\mathsf{knows}\,#1\,#2}
\newcommand\kno{\mathsf{knows}}
\newcommand\Unique[2]{\mathop{\mathsf{Unique}\,#1\mathop{\mathsf{on}}\,#2}}
\newcommand\Issues[4]{#1\,\mathop{\mathsf{Issues}}\,#2\,\mathop{\mathsf{with}}\,#3\,\mathop{\mathsf{on}}\,#4}
\newcommand\issues{\mathop{\mathsf{Issues}}}
\newcommand\with{\mathop{\mathsf{with}}}
\newcommand\on{\mathop{\mathsf{on}}}
\newcommand\evlist{\mathop{\mathsf{event~list}}}
\newcommand\event{\mathop{\mathsf{event}}}
\newcommand\msgset{\mathop{\mathsf{msg~set}}}
\newcommand\msg{\mathop{\mathit{msg}}}
\newcommand\evs{\mathop{\mathit{evs}}}
\newcommand\ev{\mathop{\mathit{ev}}}
\newcommand\rev{\mathsf{rev}}
\newcommand\takeWhile{\mathsf{takeWhile}}
\newcommand\dropWhile{\mathsf{dropWhile}}
%\newcommand\seespy{\spies{evs}}

\newcommand\initState[2]{\mathsf{initState}\,#1\,#2}
\newcommand\ini{\mathsf{initState}}
\newcommand\datatype[1]{\mathsf{datatype}~#1}
\newcommand\leg[1]{\mathsf{legallyU}#1}
\newcommand\illeg[1]{\mathsf{illegallyU}#1}
\newcommand\cons{\mathbin{\#}}

\newcommand\used{\mathop{\mathsf{used}}}
\newcommand\newN{\mathop{\mathsf{newN}}}
\newcommand\newK{\mathop{\mathsf{newK}}}
\newcommand\shrK{\mathop{\mathsf{shrK}}}
\newcommand\crdK{\mathop{\mathsf{crdK}}}
\newcommand\pubK{\mathop{\mathsf{pubK}}}
\newcommand\priK{\mathop{\mathsf{priK}}}
\newcommand\sesK{\mathop{\mathsf{sesK}}}
\newcommand\Pairkey{\mathop{\mathsf{Pairkey}}}
\newcommand\pairK{\mathop{\mathsf{pairK}}}
\newcommand\otway{\mathop{\mathsf{otway}}}
\newcommand\sol{\mathop{\mathsf{set}}}
\newcommand\image{\mathbin{``}}

\newcommand\N{\mathbf{N}}
\newcommand\Suc{\mathop{\mathsf{Suc}}}
\newcommand\nat{\mathsf{nat}}
\newcommand\agent{\mathsf{agent}}
\newcommand\msgtype{\mathsf{msg}}
%\newcommand\evs{\mathsf{evs}}


\newcommand\pin{\mathop{\mathsf{pin}}}
\newcommand\Card{\mathop{\mathsf{Card}}}
\newcommand\card{\mathsf{card}}
\newcommand\key{\mathsf{key}}
\newcommand\stolen{\mathsf{stolen}}
\newcommand\cloned{\mathsf{cloned}}
\newcommand\fake{\mathsf{Fake}}
