Updated specs

models/specification.smv

@@ -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