Commit fb4fbd96 authored by Erik Poll's avatar Erik Poll
parents 6f4008f1 028a7869
......@@ -53,8 +53,8 @@ LTLSPEC NAME trans_disc := G (out=DISCONNECT ->
---- After sending a KEXINIT, the other side should not send another KEXINIT or SR_ACCEPT until it has sent NEWKEYS
LTLSPEC NAME trans_kexinit := G ( kexStarted ->
X ( ( (out!=SR_ACCEPT & out!=KEXINIT) U receivedNewKeys |
G (out!=SR_ACCEPT & out!=KEXINIT) ) ) )
X ( ( (out!=SR_ACCEPT & !kexStarted) U receivedNewKeys |
G (out!=SR_ACCEPT & !kexStarted) ) ) )
-- If the server rejects the service request, it SHOULD send an
-- appropriate SSH_MSG_DISCONNECT message and MUST disconnect.
......@@ -63,7 +63,8 @@ LTLSPEC NAME trans_sr := G ( (inp=SR_AUTH & out!=NO_CONN & state!=s0) ->
-- If the server rejects the authentication request, it MUST respond
-- with the following: SSH_MSG_USERAUTH_FAILURE. *It may also disconnect on failed unauth attempts
LTLSPEC NAME auth_ua_pre := (invalidAuthReq -> out=UA_FAILURE ) U (out=UA_SUCCESS | connLost| kexStarted) | G (invalidAuthReq -> out=UA_FAILURE )
LTLSPEC NAME auth_ua_pre := G ( (hasReqAuth & !O out=UA_SUCCESS) ->
( (invalidAuthReq -> (out=UA_FAILURE) ) U (out=UA_SUCCESS | connLost| kexStarted ) ) | G (invalidAuthReq -> (out=UA_FAILURE | out=DISCONNECT) ) )
-- SSH_MSG_USERAUTH_SUCCESS MUST be sent only once.
LTLSPEC NAME auth_ua_post := G ( (out=UA_SUCCESS) ->
......@@ -72,7 +73,7 @@ LTLSPEC NAME auth_ua_post := G ( (out=UA_SUCCESS) ->
-- When SSH_MSG_USERAUTH_SUCCESS has been sent, any further authentication
-- requests received after that SHOULD be silently ignored. *openssh sends UNIMPL, is that bad?
LTLSPEC NAME auth_ua_post_strong := G (out=UA_SUCCESS ->
( authReq -> out=NO_RESP) U (kexStarted | connLost) )
( authReq -> out=NO_RESP) U (!authReq & (kexStarted | connLost) ) )
-- Upon receiving this message, a party MUST
......@@ -82,5 +83,5 @@ LTLSPEC NAME auth_ua_post_strong := G (out=UA_SUCCESS ->
-- the party may then reuse the channel number.
-- Had to add NEWKEYS and KEXINIT ins, strangely KEXINIT closes
LTLSPEC NAME conn_close := G ( hasOpenedChannel ->
( ( ( (inp=CH_CLOSE) -> (out=CH_CLOSE)) U (connLost | kexStarted | out=CH_CLOSE) ) |
( ( ( (inp=CH_CLOSE) -> (out=CH_CLOSE) ) U ( connLost | kexStarted ) | out=CH_CLOSE) ) |
( G ( (inp=CH_CLOSE) -> (out=CH_CLOSE)) ) ) )
\ No newline at end of file
This diff is collapsed.
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