Commit 0d1c52ce authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Specification

parent 8443a6ec
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);
-- General Properties
-- Once a connection is lost, it is lost for good
LTLSPEC NAME gen_one_conn := G (out=NO_CONN ->
G isDisconnected)
-- Cyclic behavior induced by CH_OPEN and CH_CLOSE
LTLSPEC NAME gen_cyclic := (G (inp=CH_OPEN) ->
X ( (inp=CH_OPEN -> out=CH_MAX) U (inp=CH_CLOSE & out!=CH_NONE) | G (inp=CH_OPEN -> out=CH_MAX) ) ) &
(G (inp=CH_CLOSE) ->
X ( (inp=CH_CLOSE -> out=CH_NONE) U (inp=CH_OPEN & out!=CH_MAX) | G (inp=CH_CLOSE -> out=CH_NONE) ) )
-- Security Properties
-- Transport Layer Security
LTLSPEC NAME trans_sec := G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
LTLSPEC NAME trans_sec := G ( hasReqAuth ->
O ( (inp=NEWKEYS & out=NO_RESP) &
O ( (inp=KEX30 & out=KEX31_NEWKEYS) &
O (out=KEXINIT) ) ) )
-- Authentication Layer Security
LTLSPEC NAME auth_sec := G ( (inp=CH_OPEN & out=CH_OPEN_SUCCESS) ->
LTLSPEC NAME auth_sec := G ( hasOpenedChannel ->
( out!=UA_FAILURE S out=UA_SUCCESS) )
-- Rekey Properties
-- Authenticated rekey is possible
LTLSPEC NAME auth_rekey_pos := G ( ( ( inp=CH_CLOSE & out=CH_CLOSE) | (inp=CH_OPEN & out=CH_OPEN_SUCCESS) | ( out=UA_SUCCESS) ) ->
( X (inp=KEXINIT -> out=KEXINIT & X (inp=KEX30 -> out=KEX31_NEWKEYS & X (inp=NEWKEYS -> out=NO_RESP) ) ) ) )
-- Authenticated state is preserved
LTLSPEC NAME auth_rekey_pres := G ( ( ( inp=CH_CLOSE & out=CH_CLOSE) | (inp=CH_OPEN & out=CH_OPEN_SUCCESS) | (inp=SR_AUTH & out=SR_ACCEPT) ) ->
( ( inp=NEWKEYS & out=NO_RESP & X ( inp=CH_OPEN ) ) -> X ( out=CH_OPEN_SUCCESS | out=CH_MAX) ) U (out=NO_CONN) |
( G ( ( inp=NEWKEYS & out=NO_RESP & X ( inp=CH_OPEN ) ) -> X ( out=CH_OPEN_SUCCESS | out=CH_MAX) )
& G ! (out=NO_CONN) ) )
-- Pre-auth rekey is possible
LTLSPEC NAME pre-auth_rekey_pos := G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
( X (inp=KEXINIT -> out=KEXINIT & X ( inp=KEX30 -> out=KEX31_NEWKEYS & X (inp=NEWKEYS -> out=NO_RESP) ) ) ) )
-- Functional Properties
---- Preauth state is preserved
LTLSPEC G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
( ( inp=NEWKEYS & out=NO_RESP & X ( inp=UA_PK_OK ) ) -> X ( out=UA_SUCCESS) ) U (out=NO_CONN | out=UA_SUCCESS) |
( G ( ( inp=NEWKEYS & out=NO_RESP & X ( inp=UA_PK_OK ) ) -> X ( out=UA_SUCCESS) )
& G ! (out=DISCONNECT | out=UA_SUCCESS) ) )
-- Pre-auth state is preserved
LTLSPEC NAME pre-auth_rekey_pres := G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
( ( inp=NEWKEYS & out=NO_RESP & X ( inp=UA_PK_OK ) ) -> X ( out=UA_SUCCESS) ) U (out=NO_CONN | out=UA_SUCCESS) |
( G ( ( inp=NEWKEYS & out=NO_RESP & X ( inp=UA_PK_OK ) ) -> X ( out=UA_SUCCESS) )
& G ! (out=NO_CONN | out=UA_SUCCESS) ) )
-- 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) )
-- Functional Properties
---- 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 ) |
G (out!=SR_ACCEPT & out!=KEXINIT) & G ! (out=NEWKEYS | out=KEX31_NEWKEYS ) ) ) )
G (out!=SR_ACCEPT & out!=KEXINIT) ) ) )
-- If the server rejects the service request, it SHOULD send an
-- appropriate SSH_MSG_DISCONNECT message and MUST disconnect.
......@@ -54,16 +49,19 @@ 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 ( (inp=SR_AUTH & out=SR_ACCEPT) ->
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) ) & G !(out=UA_SUCCESS | out=NO_CONN | out=DISCONNECT) ) )
G ( (inp=UA_PK_NOK -> out=UA_FAILURE) & (inp=UA_PK_OK -> out=UA_SUCCESS) ) )
-- SSH_MSG_USERAUTH_SUCCESS MUST be sent only once. 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?
-- SSH_MSG_USERAUTH_SUCCESS MUST be sent only once.
LTLSPEC NAME auth_ua_post := G ( (out=UA_SUCCESS) ->
X ( (inp=UA_PK_OK | inp=UA_PK_NOK) -> out=NO_RESP) U (out=NO_CONN) |
(G X ( (inp=UA_PK_OK | inp=UA_PK_NOK) -> out=NO_RESP) & G !(out=NO_CONN) ) )
X 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) ) )
-- Upon receiving this message, a party MUST
-- send back an SSH_MSG_CHANNEL_CLOSE unless it has already sent this
......@@ -71,6 +69,6 @@ LTLSPEC NAME auth_ua_post := G ( (out=UA_SUCCESS) ->
-- party when it has both sent and received SSH_MSG_CHANNEL_CLOSE, and
-- the party may then reuse the channel number.
-- Had to add NEWKEYS and KEXINIT ins, strangely KEXINIT closes
LTLSPEC NAME conn_close := G ( (inp=CH_OPEN & out=CH_OPEN_SUCCESS) ->
LTLSPEC NAME conn_close := G ( hasOpenedChannel ->
( ( ( (inp=CH_CLOSE) -> (out=CH_CLOSE)) U (out=NO_CONN | inp=KEXINIT | out=CH_CLOSE) ) |
( G ( (inp=CH_CLOSE) -> (out=CH_CLOSE)) & G ! (out=NO_CONN | inp=KEXINIT | out=CH_CLOSE) ) ) )
\ No newline at end of file
( 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