% File:    sec-tml-regeln.tex
% Date:    20-07-1995
% Author:  Andreas Rudloff
% Purpose: TML-Regeln unter Beruecksichtung sicherer Evaluation
%
\title{Sichere TML Evaluation}
\author{Andreas Rudloff}
\maketitle
Dieses Dokument enthaelt alle bisher definierten Regeln zur Evaluation
von TML Instruktionen. Die Regeln fuer TML-Instruktionen, die
sicherheitsrelevant sind, sind in einer entsprechend angepassten Version
aufgef\"uhrt. Diese sind durch das Wort {\sl secure} im Namen
gekennnzeichnet. Alle anderen Regeln sind vorl\"aufig unveraendert
geblieben. Aus Gr\"unden der Vollst\"andigkeit m\"ussten sie um die {\sl
Sicherheitskontexte} erweitert werden.
\begin{figure}
\begin{tabular}{rll}
$c ::=$
   & $\tmlnop                            $ & Leere Anweisung \\
$|$& $\tmlimmediate{b}                   $ & Basiswertkonstante \\
$|$& $\tmlliteral{i}                     $ & Literalkonstante \\
$|$& $\tmlgetlocal{i}                    $ & Lokaler Variablenwert \\
$|$& $\tmlgetparam{i}                    $ & Parameterwert \\
$|$& $\tmlgetglobal{i}                   $ & Wert aus dem Funktionsabschlu"s \\
$|$& $\tmlgetindexed{c_1}{c_2}           $ & Wert aus dem Objektspeicher \\
$|$& $\tmlsetlocal{i}{c_1}               $ & Lokale Variablenzuweisung \\
$|$& $\tmlsetglobal{c_1}{i}{c_2}         $ & Zuweisung an Funktionsabschlu"svari
able \\
$|$& $\tmlsetindexed{c_1}{c_2}{c_3}      $ & Variablenzuweisung im Objektspeiche
r \\
$|$& $\tmlabstract{n}{c_1}{c_2}{c_3}     $ & Anlegen eines Funktionsabschlusses
\\
$|$& $\tmllambda{c_1}{n}                 $ & Allokation lokaler Variablen \\
$|$& $\tmlapply{c_0}{c_1 \ldots c_n}     $ & Funktionsapplikation \\
$|$& $\tmlseq{c_1}{c_2}                  $ & Sequentielle Auswertung \\
$|$& $\tmlloop{c_1}                      $ & Wiederholte Auswertung \\
$|$& $\tmlexit{c_1}                      $ & Beendigung einer Wiederholung \\
$|$& $\tmltrap{c_1}{i}{c_2}              $ & Ausnahmebehandlung \\
$|$& $\tmlraise{c_1}                     $ & Erzeugen einer Ausnahme \\
$|$& $\tmlapplybuiltin{op}{c_1 \ldots c_n} $ & Aufruf einer vordefinierten Funkt
ion \\
$|$& $\k{alt}\,c_0\,\k{of}\,tags\,\k{do}$  & Fallanalyse \\
   & $c_1 \ldots c_n\,\k{else}\,c_{n+1}$   & \\
$;$& $$ & \\
$tags ::=$ & $\tmltags{n}           $ & Fallmarken \\
$;$& $$ &
\end{tabular}
\caption{Abstrakte Syntax f\"ur \TML\ Instruktionen}
\label{Abb:TML-Syntax}
\end{figure}

Die TML Instruktionen sind unver\"andert geblieben. Aus
Effizienzgr\"unden w\"are es vorstellbar, eine {\sl sichere
Funktionsanwendung} einzuf\"uhren. Diese w\"urde dann versuchen n, den
{\sl Switch-User Mechanismus} aufzurufen. Die {\sl normale}
Funktionsanwendung k\"onnte dann darauf verzichten und w\"urde damit
erheblich schneller werden. Dies bringt aber keinen
Funktionlit\"atsgewinn.

F\"ur die sichere Evaluation mu"s eine Menge {\sl Prin} eingef\"uhrt
werden, die alle zul\"assigen Principals in einer Systemumgebung
enth\"alt. Darunter gibt es einen ausgezeichneten Benutzer {\sl SSO}
(System Security Officer), unter dessen Identit\"at die
Rechteadministration erfolgt.

\begin{center}
\begin{tabular}{ll}
$c \in Code$                         & \TML\ Instruktionen \\
$i, j, k, n, m \in \NAT $            & Ganze Zahlen \\
$b \in BVal = \NAT \cup \{\tmlnil\}$ & Basiswerte \\
$op \in BFun$                        & Vordefinierte Funktionen (\engl{builtins}
) \\
$eP, rP \in \Prin$                     & Menge aller zul�ssigen Principals 
(Uids) \\
\end{tabular}
\end{center}


\begin{center}
\begin{tabular}{ll}
$\finitemap{A}{B}$                    & Endliche Abbildungen von $A$ nach $B$\\
$\mapdomain{f} $                      & Definitionsbereich einer
                                        Abbildung $f\in\finitemap{A}{B}$\\
$\maprange{f} $                       & Bildbereich einer Abbildung $f\in\finitemap{A}{B}$\\
$\makemap{} $                         & Leere Abbildung \\
$\makemap{\mapelement{a}{b}} $        & Abbildungsdefinition \\
$\makemap{\mapelement{a}{b}}(a) = b $ & Abbildungsapplikation \\
$\mapupdate{f}{g} $                   & Abbildungsmodifikation \\
\end{tabular}
\end{center}
Modifikation endlicher Abbildungen:
\[\mapdomain{\mapupdate{f}{g}} = \mapdomain{f} \cup \mapdomain{g} \]
\[\maprange{\mapupdate{f}{g}} = \maprange{f} \cup \maprange{g} \]
\[\choicetwo{(\mapupdate{f}{g})(a)} {g(a)} {falls $a\in\mapdomain{g}$}
                                    {f(a)} {sonst} \]

Jedes Objekt im Objektspeicher ist einem Besitzer zugeordnet. Um dies
abzubilden, wird die Definition eines Objektspeichers um eine Abbildung
erg\"anzt, die diese Zuordnung realisiert.
				    
\begin{center}
\begin{tabular}{rll}
$r, lit \in\Ref$       &                                       & Objektreferenze
n (\engl{references}) \\
$sv, l, p, g \in SVal$ & =$BVal \cup \Ref $                      & Zustandswerte
 (\engl{state values}) \\
$S \in Store$        & $=(\finitemap{\Ref \times \NAT}{SVal})$ & Objektspeicher
\\
                        & $\times (\finitemap{\Ref}{Code})$      &  \\
                        & $\times (\finitemap{\Ref}{\NAT})$      &  \\
                        & $\times (\finitemap{\Ref}{\Prin})$      &  \\
\end{tabular}
\end{center}

\[ \storeinit = \makestore{\makemap{}}{\makemap{}}{\makemap{}} {\makemap{}}\]

\[ \storenew{\makestore{StV}{StC}{StS}{StP}}{loc}{n}{p} = 
\makestore{StV'}{StC}{StS'}{StP'} \]
mit
\begin{eqnarray*}
r    & \not\in & \mapdomain{StV} \\
StV' & =       & StV + \makemap{\mapelement{(r,0)}{\tmlnil}}
                     + \makemap{\mapelement{(r,1)}{\tmlnil}} + \ldots
                     + \makemap{\mapelement{(r,n-1)}{\tmlnil}} \\
StS' & =       & \mapupdate{StS}{\makemap{\mapelement{r}{n}}} \\
StP' & =       & \mapupdate{StP}{\makemap{\mapelement{r}{p}}}
\end{eqnarray*}

\[ \storeget{\makestore{StV}{StC}{StS}{StP}}{r}{i} = (StV((r,i))) \]

\[ \storeset{\makestore{StV}{StC}{StS}{StP}}{r}{i}{sv} =
   \makestore{\mapupdate{StV}{\makemap{\mapelement{(r,i)}{sv}}}}{StC}{StS}{StP}
\]

\[ \storenewclosure{\makestore{StV}{StC}{StS}{StP}}{loc}{nGlob}{c}{lit}{p} =
   (\makestore{StV'}{StC'}{StS'}{StP'}, r) \]
mit
\begin{eqnarray*}
r    & \not\in & \mapdomain{StV} \\
StV' & =       & StV + \makemap{\mapelement{(r,1)}{lit}}
                     + \makemap{\mapelement{(r,2)}{\tmlnil}}
%                    + \makemap{\mapelement{(r,3)}{\tmlnil}}
                     + \ldots
                     + \makemap{\mapelement{(r,nGlob+1)}{\tmlnil}} \\
StS' & =       & \mapupdate{StS}{\makemap{\mapelement{r}{nGlob+2}}} \\
StP' & =       & \mapupdate{StP}{\makemap{\mapelement{r}{p}}}
\end{eqnarray*}

\[ \storefixexecute{\makestore{StV}{StC}{StS}{StP}}{r} = \]
\[ (StC(r), StV((r, 1)), StV((r, 2)), StV((r, 3)), \ldots, StV((r, 
StS(r)-1))) \]


Um die f\"ur die Zugriffskontrollentscheidungen notwendige Information
darzustellen, wird neben dem dynmaischen Kontext ein Sicherheitskontext
eingef\"uhrt. Dieser enth\"alt in der momentanen Version eine {\sl
effektive} und eine {\sl reale PrincipalId}. Diese repr\"asentieren die
Identit\"at des Principals, die der aktuellen Ausf\"uhrungseinheit (also
in der Regel dem aktuellen Thread) zugeordnet ist.


\begin{center}
\begin{tabular}{ll}
$\tmlenv = \tmlframe{n}{m} \in Env$     & Dynamische Kontexte \\
$\tmlseccon = \tmlsec \in SecCon$       & Sicherheitskontexte \\
$\tmllocals = [l_0 \ldots l_k] \in Loc$ & Lokale Variablenvektoren \\
$v \in Val = SVal \cup \{\tmlok,
\tmlexceptionpack{p}, \tmlexitpack{p}\}$ & Auswertungsergebnisse \\
\end{tabular}
\end{center}

F\"ur die Modellierung der sicheren Evalution werden die folgenden
beiden Funktionen benutzt:

\[\cchoicetwo{sec(eP, rP, r, owner, mode)}
            {\tmlnil}
            {f"ur Identit"aten eP und rP ist der Zugriff auf {\sl r}}
            {mit Besitzer {\sl owner} im modus {\sl mode} erlaubt}
            {exception(\tmlnil)}
            {der o.g. Zugriff ist {\bf nicht}}
            {erlaubt}\]

\begin{tabbing}
$suid(eP, rP, r) = suidP$ \hspace*{1cm} \= f"ur Identit"aten
eP und rP ist die Ausf"uhrung \\
\> von {\sl r} unter {\sl suidP} erlaubt
\end{tabbing}

Bei negativem Ergebnis einer Zugriffskontroll\"uberpr\"ufung wird eine
Exception erzeugt, die gem. der entsprechenden Regeln f\"ur Exceptions
behandelt wird.  Es erfolgt keine Aussage dar\"uber, ob es sich bei den
beiden Funktionen um TML-Funktionen oder Built-In Funktionen
handelt. Prinzipiell wird der Zugriff auf die Elemente eines
Speicherobjektes kontrolliert. Daher erfolgt beispielsweise eine
\"Uberpr\"ufung bei {\sl Eval literal secure}, da dort auf ein Element
des Literalvektors zugegriifen wird. Im Gegensatz dazu wird {\sl Eval
get param} nicht \"uberpr\"uft, daher hier nur eine OID {\sl geholt}
wird, nicht jedoch auf Elemente des referenzierten Objektes zugegriffen
wird.
\\

\define{Eval nop}{\axiom{\tmlevalnoss{\tmlnop}{\tmlok}}}

\define{Eval immediate}{\axiom{\tmlevalnoss{\tmlimmediate{b}}{b}}}

\define{Eval literal secure}{\dedone
{\tmlseceval
  {[SSO,rP]}
  {\tmlenv}
  {\tmlstore}
  {\tmllocals}
  {sec(eP, rP, r, StP(r), get)}
  {\tmlstore}
  {\tmllocals}
  {\tmlok}}
{\tmlseceval
  {[eP,rP]}
  {\tmlframe{n}{m}}
  {\tmlstore}
  {\tmllocals}
  {\tmlliteral{i}}
  {\tmlstore}
  {\tmllocals}
  {\storeget{\tmlstore}{lit}{i}}
}}

\define{Eval get local}{\axiom{\tmleval
  {\tmlenv}
  {\tmlstore}
  {[l_0 \ldots l_k]}
  {\tmlgetlocal{i}}
  {\tmlstore}
  {l_0 \ldots l_k}
  {l_{i}}
}}

\define{Eval get param}{\axiom{\tmlevalnos
  {\tmlframe{n}{m}}
  {\tmlgetparam{i}}
  {p_{i}}
}}

\define{Eval get global}{\axiom{\tmlevalnos
  {\tmlframe{n}{m}}
  {\tmlgetglobal{i}}
  {g_{i}}
}}

Die Funktionen {\sl Eval get/set indexed secure} greifen auf Elemente
von Speicherobjekten zu. Daher wird hier vor dem Zugriff eine
Zugriffskontrolle ausgef\"uhrt. Die \"Uberpr\"ufung findet jeweils
unter der Identit\"at des {\sl SS0} statt.

\define{Eval get indexed secure}{\dedthree
{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {c_1}
  {\tmlstore_2}
  {\tmllocals_2}
  {r}
}
{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_2}
  {\tmllocals_2}
  {c_2}
  {\tmlstore_3}
  {\tmllocals_3}
  {i}
}
{\tmlseceval
  {[SSO,rP]}
  {\tmlenv}
  {\tmlstore_3}
  {\tmllocals_3}
  {sec(eP, rP, r, StP(r), get)}
  {\tmlstore_3}
  {\tmllocals_3}
  {\tmlok}
}
{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlgetindexed{c_1}{c_2}}
  {\tmlstore_3}
  {\tmllocals_3}
  {\storeget{\tmlstore_3}{r}{i}}
}}


\define{Eval set local}{\ded
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {[l_0 \ldots l_k]}
  {c}
  {\tmlstore_2}
  {\tmllocals_2}
  {l}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {[l_0 \ldots l_k]}
  {\tmlsetlocal{i}{c}}
  {\tmlstore_2}
  {[l_0 \ldots l_{i-1} \, l \, l_{i+1} \ldots l_k]}
  {\tmlok}
}}

\define{Eval set indexed secure}{\dedfour
{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {c_1}
  {\tmlstore_2}
  {\tmllocals_2}
  {r}
}
{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_2}
  {\tmllocals_2}
  {c_2}
  {\tmlstore_3}
  {\tmllocals_3}
  {i}
}
{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_3}
  {\tmllocals_3}
  {c_3}
  {\tmlstore_4}
  {\tmllocals_4}
  {sv}
}
{\tmlseceval
  {[SSO,rP]}
  {\tmlenv}
  {\tmlstore_4}
  {\tmllocals_4}
  {sec(eP, rP, r, StP(r), set)}
  {\tmlstore_4}
  {\tmllocals_4}
  {\tmlok}
}
{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlsetindexed{c_1}{c_2}{c_3}}
  {\storeset{\tmlstore_4}{r}{i}{sv}}
  {\tmllocals_4}
  {\tmlok}
}}

\define{Eval abstract secure}{\dedthree
{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {c_1}
  {\tmlstore_2}
  {\tmllocals_2}
  {sv}
}
{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_2}
  {\tmllocals_2}
  {c_2}
  {\tmlstore_3}
  {\tmllocals_3}
  {lit}
}
{\storenewclosure{\tmlstore_3}{sv}{n}{c_3}{lit}{eP} = (\tmlstore_4, r)
}
{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlabstract{n}{c_1}{c_2}{c_3}}
  {\tmlstore_4}
  {\tmllocals_3}
  {r}
}}

\define{Eval set global}{\ded
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlsetindexed{c_1}{\tmlimmediate{i+2}}{c_2}}
  {\tmlstore_2}
  {\tmllocals_2}
  {v}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlsetglobal{c_1}{i}{c_2}}
  {\tmlstore_2}
  {\tmllocals_2}
  {v}
}}

\define{Eval lambda}{\ded
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {[\overbrace{\tmlnil \ldots \tmlnil}^k]}
  {c}
  {\tmlstore_2}
  {\tmllocals_2}
  {v}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmllambda{c}{k}}
  {\tmlstore_2}
  {\tmllocals_1}
  {v}
}}

Die Instruktion {\sl Eval apply secure} ist entscheidend f\"ur den {\sl
Switch-user Mechanismus}. Daher werden vor der Funktionsanwendung zwei
Bedingungen gepr\"uft:
\begin{enumerate}
\item Darf der Benutzer das Objekt, also die Closure, f\"ur einen {\sl
Call} benutzen?
\item Unter welcher Identit\"at soll die Funktion ausgef\"uhrt werden? In
der Regel werden sichere Funktionen unter der Identi\"at des Besitzers der
Closure ausgef\"uhrt, alle anderen unter der Identi\"at des Aufrufers.
\end{enumerate}

\define{Eval apply secure}{\dedsix
{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {c}
  {\tmlstore_2}
  {\tmllocals_2}
  {r}
}
{\storefixexecute{\tmlstore_2}{r} = (c',lit, g_0, \ldots, g_n)
}
{{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_{i+2}}
  {\tmllocals_{i+2}}
  {c_i}
  {\tmlstore_{i+3}}
  {\tmllocals_{i+3}}
  {p_i}
}  \bigspc i = 0 \ldots m}
{\tmlseceval
  {[SSO,rP]}
  {\tmlenv}
  {\tmlstore_{m+3}}
  {\tmllocals_{m+3}}
  {sec(eP, rP, r, StP(r), call)}
  {\tmlstore_{m+3}}
  {\tmllocals_{m+3}}
  {\tmlok}
}
{\tmlseceval
  {[SSO,rP]}
  {\tmlenv}
  {\tmlstore_{m+3}}
  {\tmllocals_{m+3}}
  {suid(eP, rP, r)}
  {\tmlstore_{m+3}}
  {\tmllocals_{m+3}}
  {suidP}
}
{\tmlseceval
  {[suidP,rP]}
  {\tmlframe{n}{m}}
  {\tmlstore_{m+3}}
  {\tmllocals_{m+3}}
  {c'}
  {\tmlstore}
  {\tmllocals_{m+3}}
  {v}
}
{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {c(c_0 \ldots c_m)}
  {\tmlstore}
  {\tmllocals_{m+3}}
  {v}
}}

Prinzipiell w\"are f\"ur {\sl Eval apply secure} auch eine Modellierung
denkbar, die auf die {\sl sec-}\"Uberpr\"ufung verzichtet. Dann m\"usste
die {\sl suid-}Funktion vor dem {\sl fixexecute} aufgerufen werden und
alle anderen Vorbedingungen m\"u"sten entsprechend {\sl suidP} als
effektiven Principal benutzen. Zudem m\"usste {\sl fixececute} deutlich
auf store.get zur\"uckgef\"uhrt werden.

Bei den Built-In Funktion mu"s ber\"ucksichtigt werden, ob sie zu ihrer
Ausf\"uhrung Informationen aus dem Sicherheitskontext ben\"otigen. F\"ur
alle Built-In Funktionen, die entsprechende Information ben\"otigen,
wird eine eigene Regel definiert.

Dabei f\"allt meines Erachtens aber auch auf, da"s auf die sicheren
Varianten f\"ur die Regeln {\sl Eval get/set indexed} verzichtet werden
k\"onnte, da sie ja auf die entsprechenden {\sl store.get/set}
Operationen zur\"uckgef\"uhrt werden, die ihrerseits die
Zugriffskontroll\"uberpr\"ufung durchf\"uhren. Allerdings ist die
Verwendung der sicheren {\sl Eval get/set indexed} Regeln wohl offensichtlicher.
\\

$BuiltInSecure = \{store.new, store.set, store.get\}$
\\

\define{Eval apply builtin secure}{\dedthree
{{\tmleval
  {\tmlenv}
  {\tmlstore_{i+1}}
  {\tmllocals_{i+1}}
  {c_i}
  {\tmlstore_{i+2}}
  {\tmllocals_{i+2}}
  {p_i}
} \bigspc i = 0 \ldots m}
{op \not\in BuiltInSecure}
{apply_{op}(\tmlstore_{m+2}, p_0, \ldots, p_m) = (\tmlstore, v)}
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlapplybuiltin{op}{c_0 \ldots c_m}}
  {\tmlstore}
  {\tmllocals_{m+2}}
  {v}
}}

\define{Eval apply builtin secure \storenewNoParam}{\dedthree
{{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_{i+1}}
  {\tmllocals_{i+1}}
  {c_i}
  {\tmlstore_{i+2}}
  {\tmllocals_{i+2}}
  {p_i}
} \bigspc i = 0 \ldots 2}
{op = \storenewNoParam}
{apply_{\storenewNoParam}(\tmlstore_{4}, p_0, \ldots, p_2, eP) = (\tmlstore, v)}
{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlapplybuiltin{op}{c_0 \ldots c_3}}
  {\tmlstore}
  {\tmllocals_{4}}
  {v}
}}

\define{Eval apply builtin secure \storesetNoParam}{\dedfour
{{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_{i+1}}
  {\tmllocals_{i+1}}
  {c_i}
  {\tmlstore_{i+2}}
  {\tmllocals_{i+2}}
  {p_i}
} \bigspc i = 0 \ldots 3}
{op = \storesetNoParam}
{\tmlseceval
  {[SSO,rP]}
  {\tmlenv}
  {\tmlstore_5}
  {\tmllocals_5}
  {sec(eP, rP, r, StP(r), set)}
  {\tmlstore_5}
  {\tmllocals_5}
  {\tmlok}
}
{apply_{\storesetNoParam}(\tmlstore_5, p_0, \ldots, p_3) = (\tmlstore, v)}
{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlapplybuiltin{op}{c_0 \ldots c_4}}
  {\tmlstore}
  {\tmllocals_{5}}
  {v}
}}

\define{Eval apply builtin secure \storegetNoParam}{\dedfour
{{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_{i+1}}
  {\tmllocals_{i+1}}
  {c_i}
  {\tmlstore_{i+2}}
  {\tmllocals_{i+2}}
  {p_i}
} \bigspc i = 0 \ldots 2}
{op = \storegetNoParam}
{\tmlseceval
  {[SSO,rP]}
  {\tmlenv}
  {\tmlstore_4}
  {\tmllocals_4}
  {sec(eP, rP, r, StP(r), get)}
  {\tmlstore_4}
  {\tmllocals_4}
  {\tmlok}
}
{apply_{\storegetNoParam}(\tmlstore_{4}, p_0, \ldots, p_2) = (\tmlstore, v)}
{\tmlseceval
  {[eP,rP]}
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlapplybuiltin{op}{c_0 \ldots c_m}}
  {\tmlstore}
  {\tmllocals_{4}}
  {v}
}}

\define{Eval alt}{\dedtwo
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {c}
  {\tmlstore_2}
  {\tmllocals_2}
  {b_j}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_2}
  {\tmllocals_2}
  {c_{i_j}}
  {\tmlstore_3}
  {\tmllocals_3}
  {v}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlalt{c}{\tmltags{n}}{\tmlbranches{m}}{c'}}
  {\tmlstore_3}
  {\tmllocals_3}
  {v}
}}

\define{Eval alt else}{\dedthree
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {c}
  {\tmlstore_2}
  {\tmllocals_2}
  {v}
}
{\forall 1 \leq j \leq n : v \neq b_j }
{\tmleval
  {\tmlenv}
  {\tmlstore_2}
  {\tmllocals_2}
  {c'}
  {\tmlstore_3}
  {\tmllocals_3}
  {v'}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlalt{c}{\tmltags{n}}{\tmlbranches{m}}{c'}}
  {\tmlstore_3}
  {\tmllocals_3}
  {v'}
}}

\define{Eval seq}{\dedtwo
{\tmleval
  {\tmlenv}
  {\tmlstore_{1}}
  {\tmllocals_{1}}
  {c_1}
  {\tmlstore_{2}}
  {\tmllocals_{2}}
  {v}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_{2}}
  {\tmllocals_{2}}
  {c_2}
  {\tmlstore_{3}}
  {\tmllocals_{3}}
  {v'}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlseq{c_1}{c_2}}
  {\tmlstore_3}
  {\tmllocals_3}
  {v'}
}}

\define{Eval exit}{\ded
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {c}
  {\tmlstore_2}
  {\tmllocals_2}
  {p}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlexit{c}}
  {\tmlstore_2}
  {\tmllocals_2}
  {\tmlexitpack{p}}
}}

\define{Eval loop}{\dedthree
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {c}
  {\tmlstore_2}
  {\tmllocals_2}
  {v_1}
}
{v_1 \in SVal \cup \{\tmlok\}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_2}
  {\tmllocals_2}
  {\tmlloop{c}}
  {\tmlstore_3}
  {\tmllocals_3}
  {v_2}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlloop{c}}
  {\tmlstore_3}
  {\tmllocals_3}
  {v_2}
}}

\define{Eval loop exit}{\ded
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {c}
  {\tmlstore_2}
  {\tmllocals_2}
  {\tmlexitpack{p}}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlloop{c}}
  {\tmlstore_2}
  {\tmllocals_2}
  {p}
}}

\define{Eval raise}{\ded
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {c}
  {\tmlstore_2}
  {\tmllocals_2}
  {p}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlraise{c}}
  {\tmlstore_2}
  {\tmllocals_2}
  {\tmlexceptionpack{p}}
}}

\define{Eval trap}{\dedtwo
{\tmleval
  {\tmlenv}
  {\tmlstore_{1}}
  {\tmllocals_{1}}
  {c_1}
  {\tmlstore_{2}}
  {\tmllocals_{2}}
  {v}
}
{v \neq \tmlexceptionpack{p}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmltrap{c_1}{i}{c_2}}
  {\tmlstore_2}
  {\tmllocals_2}
  {v}
}}

\define{Eval trap exception}{\dedtwo
{\tmleval
  {\tmlenv}
  {\tmlstore_{1}}
  {\tmllocals_{1}}
  {c_1}
  {\tmlstore_{2}}
  {[l_0 \ldots l_k]}
  {\tmlexceptionpack{p}}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_{2}}
  {[l_0 \ldots l_{i-1} \, p \, l_{i+1} \ldots l_k]}
  {c_2}
  {\tmlstore_{3}}
  {\tmllocals_{3}}
  {v_2}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmltrap{c_1}{i}{c_2}}
  {\tmlstore_3}
  {\tmllocals_3}
  {v_2}
}}

\dedthreeh
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {c_1}
  {\tmlstore'_1}
  {\tmllocals'_1}
  {v_1}
}
{ \ldots
}
{\tmleval
  {\tmlenv}
  {\tmlstore_n}
  {\tmllocals_n}
  {c_n}
  {\tmlstore'_n}
  {\tmllocals'_n}
  {v_n}
}
{\tmleval
  {\tmlenv}
  {\tmlstore}
  {\tmllocals}
  {c}
  {\tmlstore'}
  {\tmllocals'}
  {v'}
}

\ \\ \noindent und f"ur jedes $k, 1 \leq k \leq n$, f"ur das das
Ergebnis $v_k$ kein Exit- oder Ausnahmepaket ist, ist eine zus"atzliche
Regel der folgenden Form einzuf"ugen:
\ \\

\dedtwo
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {c_1}
  {\tmlstore'_1}
  {\tmllocals'_1}
  {v_1}
  \bigspc \ldots \bigspc
 \tmleval
  {\tmlenv}
  {\tmlstore_k}
  {\tmllocals_k}
  {c_k}
  {\tmlstore'_k}
  {\tmllocals'_k}
  {v_k}
}
{ \bigspc v_k = \tmlexitpack{p} \vee v_k = \tmlexceptionpack{p}
}
{\tmleval
  {\tmlenv}
  {\tmlstore}
  {\tmllocals}
  {c}
  {\tmlstore'_k}
  {\tmllocals'_k}
  {v_k}
}

\newpage

{\bf Abschliessende Bemerkungen:}

\begin{itemize}
\item Die o.g. {\sl Sicherheitsfunktionen} sowie die Authentisierung
selbst sind hier nicht spezifiziert, da es sich nicht um {\sl atomare}
TML-Funktionen handelt. Damit \"urden wir letztendlich im Bereich
formaler Spezifikationen landen, wo wir wohl nicht hinwollen (vermute
ich).

\item Im Grunde k\"onnten noch einige {\sl Thread-Funktionen}, z.B. {\tt
thread\_new, thread\_run} spezifiziert werden. Die Spezifikation w\"urde
sich allerdings auch nur auf die Konstruktion des Sicherheitskontextes
beziehen.
\end{itemize}