Specification

models/specification.smv

@@ -2,6 +2,7 @@ DEFINE isDisconnected := (out=NO_CONN | out=CH_MAX | out=CH_NONE);
 DEFINE hasReqAuth := (inp=SR_AUTH & out=SR_ACCEPT);
 DEFINE hasOpenedChannel := (out=CH_OPEN_SUCCESS);
 DEFINE hasAuth := (out=UA_PK_OK | out=UA_PK_OK);
+DEFINE authReq := (inp=UA_PK_OK | inp=UA_PW_OK | inp=UA_PK_NOK | inp=UA_PW_NOK | inp=UA_NONE);
 
 
 
@@ -45,13 +46,13 @@ LTLSPEC NAME trans_kexinit := G ( (out=KEXINIT) ->
 -- If the server rejects the service request, it SHOULD send an
 -- appropriate SSH_MSG_DISCONNECT message and MUST disconnect. 
 LTLSPEC NAME trans_sr := G ( (inp=SR_AUTH & out!=NO_CONN & state!=s0) -> 
-    (out=SR_ACCEPT | (out=DISCONNECT & X G(inp=SR_AUTH -> out=NO_CONN) ) ) )
+    (out=SR_ACCEPT | out=DISCONNECT ) )
     
 -- 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 := G ( hasReqAuth ->
-  ( (inp=UA_PK_NOK -> out=UA_FAILURE) & (inp=UA_PK_OK -> out=UA_SUCCESS) ) U (out=UA_SUCCESS | out=NO_CONN | out=DISCONNECT) |
-  G ( (inp=UA_PK_NOK -> out=UA_FAILURE) & (inp=UA_PK_OK -> out=UA_SUCCESS) ) ) 
+  (inp=UA_PK_NOK | inp=UA_PW_NOK | inp=UA_NONE -> out=UA_FAILURE ) U (out=UA_SUCCESS | out=NO_CONN | out=DISCONNECT) |
+  G (inp=UA_PK_NOK | inp=UA_PW_NOK | inp=UA_NONE -> out=UA_FAILURE ) ) 
 
 -- SSH_MSG_USERAUTH_SUCCESS MUST be sent only once. 
 LTLSPEC NAME auth_ua_post := G ( (out=UA_SUCCESS) ->
@@ -60,7 +61,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 ->
-    X ( ( (inp=UA_PK_OK | inp=UA_PK_NOK) -> out=NO_RESP | out=NO_CONN) ) )
+    X ( ( authReq -> out=NO_RESP | out=NO_CONN) ) )
 
     
 -- Upon receiving this message, a party MUST