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

Updated specification. Found small error

parent 351f97fe
...@@ -73,7 +73,7 @@ LTLSPEC NAME auth_ua_post := G ( (out=UA_SUCCESS) -> ...@@ -73,7 +73,7 @@ LTLSPEC NAME auth_ua_post := G ( (out=UA_SUCCESS) ->
-- When SSH_MSG_USERAUTH_SUCCESS has been sent, any further authentication -- 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? -- requests received after that SHOULD be silently ignored. *openssh sends UNIMPL, is that bad?
LTLSPEC NAME auth_ua_post_strong := G (out=UA_SUCCESS -> LTLSPEC NAME auth_ua_post_strong := G (out=UA_SUCCESS ->
( authReq -> out=NO_RESP) U (!authReq & (kexStarted | connLost) ) ) X ( ( authReq -> out=NO_RESP) U (!authReq & (kexStarted | connLost) ) | G (authReq -> out=NO_RESP) ) )
-- Upon receiving this message, a party MUST -- Upon receiving this message, a party MUST
...@@ -83,5 +83,5 @@ LTLSPEC NAME auth_ua_post_strong := G (out=UA_SUCCESS -> ...@@ -83,5 +83,5 @@ LTLSPEC NAME auth_ua_post_strong := G (out=UA_SUCCESS ->
-- the party may then reuse the channel number. -- the party may then reuse the channel number.
-- Had to add NEWKEYS and KEXINIT ins, strangely KEXINIT closes -- Had to add NEWKEYS and KEXINIT ins, strangely KEXINIT closes
LTLSPEC NAME conn_close := G ( hasOpenedChannel -> 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)) ) ) ) ( G ( (inp=CH_CLOSE) -> (out=CH_CLOSE)) ) ) )
\ No newline at end of file
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