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

updated spec

parent 1b243f09
-- Security Properties
-- Transport Layer Security
LTLSPEC NAME trans_sec := G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
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) ->
( 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) ) ->
......@@ -23,16 +28,16 @@ LTLSPEC NAME pre-auth_rekey_pos := G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
---- 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) ) )
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) ) )
& G ! (out=NO_CONN | out=UA_SUCCESS) ) )
......
Supports Markdown
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