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

Updated specifications. Added many more predicates.

parent 0748ffda
DEFINE isDisconnected := (out=NO_CONN | out=CH_MAX | out=CH_NONE);
DEFINE isSilent := (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_PW_OK);
DEFINE authReq := (inp=UA_PK_OK | inp=UA_PW_OK | inp=UA_PK_NOK | inp=UA_PW_NOK | inp=UA_NONE);
DEFINE validAuthReq := (inp=UA_PK_OK | inp=UA_PW_OK);
DEFINE invalidAuthReq := (inp=UA_PK_NOK | inp=UA_PW_NOK | inp=UA_NONE);
DEFINE receivedNewKeys := (out=NEWKEYS | out=KEX31_NEWKEYS);
DEFINE kexStarted := (out=KEXINIT);
DEFINE connLost:= out=NO_CONN | out=DISCONNECT;
-- General Properties
-- Once a connection is lost, it is lost for good
LTLSPEC NAME gen_one_conn := G (out=NO_CONN ->
G isDisconnected)
G isSilent)
-- Cyclic behavior induced by CH_OPEN and CH_CLOSE
LTLSPEC NAME gen_cyclic := (G (inp=CH_OPEN) ->
......@@ -23,24 +27,33 @@ LTLSPEC NAME gen_cyclic := (G (inp=CH_OPEN) ->
LTLSPEC NAME trans_sec := G ( hasReqAuth ->
O ( (inp=NEWKEYS & out=NO_RESP) &
O ( (inp=KEX30 & out=KEX31_NEWKEYS) &
O (out=KEXINIT) ) ) )
O kexStarted ) ) )
-- Authentication Layer Security
LTLSPEC NAME auth_sec := G ( hasOpenedChannel ->
( out!=UA_FAILURE S out=UA_SUCCESS) )
-- Rekey properties
-- Pre-auth rekey is possible
LTLSPEC NAME pre-auth_rekey_pos := G ( hasReqAuth ->
X (inp=KEXINIT -> out=KEXINIT & X ( inp=KEX30 -> out=KEX31_NEWKEYS & X (inp=NEWKEYS -> out=NO_RESP) ) ) U
(connLost | hasAuth | kexStarted) | G X (inp=KEXINIT -> out=KEXINIT & X ( inp=KEX30 -> out=KEX31_NEWKEYS & X (inp=NEWKEYS -> out=NO_RESP) ) ) )
-- Authenticated rekey is possible
LTLSPEC NAME auth_rekey_pos := G ( hasOpenedChannel ->
X (inp=KEXINIT -> out=KEXINIT & X (inp=KEX30 -> out=KEX31_NEWKEYS & X (inp=NEWKEYS -> out=NO_RESP) ) ) U (connLost | kexStarted) |
G X (inp=KEXINIT -> out=KEXINIT & X (inp=KEX30 -> out=KEX31_NEWKEYS & X (inp=NEWKEYS -> out=NO_RESP) ) ) )
-- Functional Properties
-- Server sends DISCONNECT:
-- The sender MUST NOT send or receive any data after this message, and
-- the recipient MUST NOT accept any data after receiving this message.
LTLSPEC NAME trans_disc := G (out=DISCONNECT ->
X G (isDisconnected) )
X G (isSilent) )
---- 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 ( (out=KEXINIT) ->
X ( ( (out!=SR_ACCEPT & out!=KEXINIT) U (out=NEWKEYS | out=KEX31_NEWKEYS ) |
LTLSPEC NAME trans_kexinit := G ( kexStarted ->
X ( ( (out!=SR_ACCEPT & out!=KEXINIT) U receivedNewKeys |
G (out!=SR_ACCEPT & out!=KEXINIT) ) ) )
-- If the server rejects the service request, it SHOULD send an
......@@ -50,9 +63,7 @@ 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 := G ( hasReqAuth ->
(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 ) )
LTLSPEC NAME auth_ua_pre := (invalidAuthReq -> out=UA_FAILURE ) U (out=UA_SUCCESS | connLost| kexStarted) | G (invalidAuthReq -> out=UA_FAILURE )
-- SSH_MSG_USERAUTH_SUCCESS MUST be sent only once.
LTLSPEC NAME auth_ua_post := G ( (out=UA_SUCCESS) ->
......@@ -61,7 +72,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 ( ( authReq -> out=NO_RESP | out=NO_CONN) ) )
( authReq -> out=NO_RESP) U (kexStarted | connLost) )
-- Upon receiving this message, a party MUST
......@@ -71,5 +82,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 (out=NO_CONN | inp=KEXINIT | 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
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