Commit 97388517 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

More edits

parent ca56c4a7
......@@ -39,8 +39,10 @@ G ( (input= CH_OPEN & output= CH_OPEN_SUCCESS)
\caption{User Authentication layer LTL in NuSMV syntax.}
\end{figure}
\paragraph{Result:} both systems appear to respect this property.
\subsection{Re-key properties}
An important property is that re-exchanging keys can be done in any state of the protocol, and its successful execution doesn't change the protocol state. We consider 2 general protocol states, pre-authenticated (after a successful authentication request, before authentication) and authenticated. For these, we specify that performing key exchange should always preserve the state, until specific inputs or outputs are encountered that necessarily change it. An example of such inputs or outputs are those corresponding to a disconnect action from either side.
An important property is that re-exchanging keys can be performed in any state of the protocol, and its successful execution doesn't change the protocol state. We consider 2 general protocol states, pre-authenticated (after a successful authentication request, before authentication) and authenticated. For these, we specify that performing key exchange should always preserve the state, until specific inputs or outputs are encountered that necessarily change it. An example of such inputs or outputs are those corresponding to a disconnect action from either side.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment