--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/semantics/pysec.sty	Mon May 18 09:56:21 2009 +0200
@@ -0,0 +1,75 @@
+ \ProvidesPackage{pysec}
+
+%% ----------------------------------------
+
+\newcommand{\nt}[1]{{\it #1}}
+
+
+\newlength{\CLCodeIndent}
+\setlength{\CLCodeIndent}{1em}
+\newlength{\CLParSkip}
+\setlength{\CLParSkip}{\parskip}
+\def\Code{\list{}{\leftmargin \CLCodeIndent
+                      \itemindent\listparindent
+                      \parsep 0pt plus 1pt}\item
+                      \begingroup\CLInnerMacros\tabbing}
+\makeatletter
+% Need to be slightly different from \endtabbing
+\def\endCode{\unskip\@stopfield\@addfield\ifdim\wd\@curline>0pt\@startfield\@stopline\fi
+  \ifnum\@tabpush >\z@ \@badpoptabs \fi\endtrivlist\endgroup\endlist}
+
+\newcommand\CLMathsurround{\mathsurround=0.166666em}
+\newcommand\SmallCLMathsurround{\mathsurround=0.083333em}
+\newcommand\KWD[1]{{\ensuremath{\mathtt{#1}\CLMathsurround}}}
+\newcommand\TYP[1]{{\ensuremath{\mathrm{#1}\SmallCLMathsurround}}}
+\newcommand\VAR[1]{{\ensuremath{\mathit{#1}\SmallCLMathsurround}}}
+\newcommand\STR[1]{{\ensuremath{\hbox{\tt#1}\CLMathsurround}}}
+\newcommand\EXP[1]{{\ensuremath{{\protect\CLInnerMacros#1}\CLMathsurround}}}
+\newcommand\CLInnerKWD[1]{\mathrel{\mathtt{#1}}}
+\newcommand\CLInnerOPR[1]{\mathbin{\mathtt{#1}}}
+\newcommand\CLInnerTYP[1]{\mathord{\mathrm{#1}}}
+\newcommand\CLInnerVAR[1]{\mathord{\mathit{#1}}}
+\newcommand\CLInnerSTR[1]{{\tt#1}}
+\newcommand\JOIN{{\ensuremath{\text{JOIN}}}}
+\newcommand\env{{\ensuremath{\text{secret}_s}}}
+\newcommand\SECRET{{\ensuremath{\text{secret}_e}}}
+\newcommand\error{{\ensuremath{\text{error}}}}
+
+\newcommand\CLInnerMacros{\let\KWD\CLInnerKWD\let\OPR\CLInnerOPR
+  \let\TYP\CLInnerTYP\let\VAR\CLInnerVAR\let\STR\CLInnerSTR}
+
+
+
+
+\newcommand{\metavar}[1]{\ensuremath{\mathrm{#1}}}
+\newcommand{\set}[1]{\ensuremath{\mathcal{#1}}}
+\newcommand{\Values}{\ensuremath{\mathcal{V}}}
+
+\newcommand{\LL}{\mbox{$[\![$}}
+\newcommand{\RR}{\mbox{$]\!]$}}
+
+\newsavebox{\tmpbox}
+\newenvironment{boxeddisp}[1]
+  {\addtolength{\fboxsep}{1ex}\begin{center}\addtolength{\linewidth}{-2\fboxsep}%
+    \addtolength{\linewidth}{-2\fboxrule}%
+    \begin{lrbox}{\tmpbox}\begin{minipage}{#1}%
+   \abovedisplayskip=0pt}
+  {\end{minipage}\end{lrbox}%
+    \framebox{\usebox{\tmpbox}}\vspace{-0.3cm}\end{center}}
+
+\newcommand{\aboveleftarrow}[1]
+{\stackrel{#1}{\longleftarrow}}
+
+\newcommand{\aboverightarrow}[1]
+{\stackrel{#1}{\longrightarrow}}
+
+\newcommand{\aboveLeftarrow}[1]
+{\stackrel{#1}{\Longleftarrow}}
+
+\newcommand{\aboveRightarrow}[1]
+{\stackrel{#1}{\Longrightarrow}}
+
+\newcommand{\emptyline}{\vspace{0.2in}}
+
+\newcommand{\secret}[1]
+{\setlength\fboxsep{1pt}\fbox{\ensuremath{#1}}\setlength\fboxsep{3pt}}