Commit 40274912 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Updated security definitions

parent aaddb03a
......@@ -88,7 +88,7 @@ A key note is that properties are checked not on the actual concrete model of th
Before introducing the properties, we mention some basic predicates and conventions we use in their definition. The happy flow in SSH consists in a series of steps, the user first exchanges keys, then requests for the authentication service, followed up by supplying valid credentials and authentication, concluded by opening of a channel. Whereas the first step is complex, the subsequent steps can be captured by the simple predicates {\dreqauth} , {\dauth} and {\dopchan} respectively. The predicates are defined in terms of the output generated at a given moment, with certain values of this output indicating that the step was performed successfully. For example, \textsc{ch\_open\_success} indicates that a channel has been opened successfully. Sometimes, we also need the input that generated the output, in order to distinguish this step from a different step. In particular, requesting the authentication service is distinguished from requesting the connection service by \textsc{sr\_auth}.
hasReqAuth := inp=SR_AUTH & out=SR_ACCEPT
hasAuth := out=UA_PK_OK | out=UA_PW_OK
hasOpenedChannel := out=CH_OPEN_SUCCESS
Supports Markdown
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