Algorithmus

In diesem Abschnitt soll eine Algorithmus beschrieben werden, der für einen gegebenes Name-Stamp Protokoll $T = \{\alpha_i,\beta_i\}$ und einer Eingabenlänge

$$n = \sum_i l(\alpha_i) + \sum_j l(\beta_j)$$

in ${\cal O}(n^8)$ bestimmt, ob das Protokoll sicher ist. Hierfür zunächst einige Festlegungen.

Definition 18 (nicht reduzierbare Wortmengen)
Seien $X$ und $Y$ Teilnehmer eines Name-Stamp Protokolls und

$$\eta \in W(\{E_a,D_a,i_a\;\vert\;A \in \{X,Y\}\})$$

nicht weiter reduzierbar. Dann ist $C(\eta)$ die Menge aller nicht reduzierbaren Wörter

$$\delta \in W(\{E_a,D_a,i_a,d_a\;\vert\;A\;-\;Teilnehmer\})$$

mit $\overline{\delta\eta} = \lambda$.

Definition 19 (Wortmenge $S$)
Seien $X$, $Y$ Teilnehmer eines Name-Stamp Protokolls $T=\{\alpha_i,\beta_j\}$.

$$\begin{eqnarray*} S & := & \{\alpha_i\;\vert\;A,B \in \{X,Y,Z\}, A \neq B, i \ge... ...\{E_a,i_a,d_a\;\vert\;A \in \{X,Y,Z\}\} \\ & \cup & \{D_z\} \\ \end{eqnarray*}$$

Seien $X$ und $Y$ Teilnehmer eines Name-Stamp Protokolls. Dann leistet der folgende Algorithmus das gewünschte.

CheckSecurity( $T=\{\alpha_i,\beta_j\}$)
1	$M := \{\overline{N_i(X,Y)}\;\vert\;1\leq i \leq 2 \cdot t \}$
2	for $\rho \in M$ do
3	for $\gamma \in S^\star$ do
4	if $\overline{\gamma} \in C(\rho)$ then return false
5	end
6	end
7	return true
8	end

In [1] ist ein Beweis angegeben. Für den vollständigen Beweis wird ein Teil des Problems also die Frage ($\rho \in M$ wie oben):

$$\exists_{\gamma \in S^\star}:\;\overline{\gamma} \in C(\rho)$$

unter Nutzung einer Grammatik in das Worterweiterungsproblem überführt. Zum Verständnis dieses hier nicht aufgeführten Beweises empfehle ich z.B. [3] zu Hilfe zu nehmen.