Finish(?) SSH example

2 files changed, 8 insertions, 10 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 9d956b6..72304d2 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -145,6 +145,7 @@ The final step of the algorithm entails removing the parts of the formula that c
 
 \camil
 \begin{example}[Properties for an Authentication System]
+	\label{ex:pltl-to-ltl:authentication}
 	Consider again the property from \cref{ex:pltl:authentication-system}, repeated here with less verbose names:
 	$\phi = \square (c \rightarrow \lnot f \Sop s)$.
 	This can be rewritten to a form with only $\Uop$ and $\Sop$:
@@ -254,8 +255,7 @@ The final step of the algorithm entails removing the parts of the formula that c
 		\item $\square\lnot(f \land \psi)$.
 			After an authentication failure, a connection cannot be established without prior authentication success.
 	\end{itemize}
-	We see that the formula is reasonably succinct compared to its PLTL version, $\square(c \rightarrow \lnot f \Sop s)$.
-	Using past modalities was not needed in this case.
+	The resulting LTL formula is reasonably succinct, but is clear that the PLTL formula is easier to construct and understand.
 \end{example}
 
 \erin
diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex
index 42ebf63..8543669 100644
--- a/Assignment1/syntax.tex
+++ b/Assignment1/syntax.tex
@@ -170,13 +170,11 @@ Before turning to the formal semantics in the next subsection, we provide some e
 	One property says that if a channel is opened, there must have been some successful authentication attempt in the past~\citep[p.~149]{FiterauBrostean2017}.
 	Also, since that successful authentication, no authentication failure must have occurred.
 	This formula is intuitively expressed by $\square(\textsl{hasOpenedChannel} \rightarrow \lnot \textsl{authFailure} \Sop \textsl{authSuccess})$.
-	Expressing this property in LTL is obscure and tedious.
-	One way uses the Weak Until operator from Section 5.1.5:
-	%TODO please check that this is actually equivalent
-	\begin{align*}
-		& \lnot \textsl{hasOpenedChannel} \Wop\\
-		& \quad (\textsl{authSuccess} \land (\square \textsl{authFailure} \rightarrow \lnot \textsl{hasOpenedChannel} \Uop \textsl{authSuccess}))
-		\qedhere
-	\end{align*}
+	An equivalent LTL formula is $\lnot \psi \land \square\lnot(\textsl{authFailure} \land \psi)$,
+		where $\psi = \lnot\textsl{authSuccess} \Uop (\textsl{hasOpenedChannel} \land \lnot\textsl{authSuccess})$.
+	If $\psi$ holds, a channel will be opened without prior authentication success.
+	Therefore, $\psi$ should not hold at the beginning or when authentication fails.
+	The LTL formula is derived algorithmically in \cref{ex:pltl-to-ltl:authentication}.
+	The LTL formula is slightly larger than the PLTL formula and is slightly less understandable.
 \end{example}
 \cbend