diff options
Diffstat (limited to 'Assignment1/syntax.tex')
| -rw-r--r-- | Assignment1/syntax.tex | 14 |
1 files changed, 6 insertions, 8 deletions
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 |