From cd60bdeb0ec968ba3fafa8959a1b9d5cd744432f Mon Sep 17 00:00:00 2001 From: Douglas Stebila Date: Thu, 4 Nov 2021 12:21:06 -0400 Subject: [PATCH] Use macros for transcripts --- Makefile | 3 + corekt.spthy | 3 + glossary.md | 3 +- lemmas/reachable.spthy | 92 +++++------------------------ protocol/kemtls_sauth_client.spthy | 52 ++++++++-------- protocol/kemtls_sauth_defines.spthy | 7 +++ protocol/kemtls_sauth_server.spthy | 46 +++++++-------- 7 files changed, 80 insertions(+), 126 deletions(-) create mode 100644 protocol/kemtls_sauth_defines.spthy diff --git a/Makefile b/Makefile index 35dc4e9..4ff49f6 100644 --- a/Makefile +++ b/Makefile @@ -8,3 +8,6 @@ well-formed: preprocess prove: preprocess tamarin-prover $(if $(PROVE), --prove=$(PROVE), --prove) generated_corekt.spthy + +clean: + $(RM) -f generated_* */generated_* diff --git a/corekt.spthy b/corekt.spthy index 5172a09..eb6b0ef 100644 --- a/corekt.spthy +++ b/corekt.spthy @@ -1,9 +1,12 @@ +changequote() + theory corekt begin include(protocol/primitives.spthy) include(protocol/kemtls_keygen.spthy) +include(protocol/kemtls_sauth_defines.spthy) include(protocol/kemtls_sauth_client.spthy) include(protocol/kemtls_sauth_server.spthy) diff --git a/glossary.md b/glossary.md index c61986a..444f795 100644 --- a/glossary.md +++ b/glossary.md @@ -72,6 +72,7 @@ For KEMTLS, `stage` can be `'1'`, `'2'`, ..., `'6'`. - `Auth(tid, stage)`: Records that thread `tid` has accepted the stage `stage` key as authenticated. - `RevealedSessionKey(tid, stage)`: Records that the stage `stage` key in thread `tid` was revealed to the adversary. - `CorruptedLTK(P)`: Records that party `P`'s long-term secret key was revealed to the adversary. +- `ProtocolMode(tid, mode)`: Records that thread `tid` is running in protocol mode `mode` (one of: `KEMTLS_SAUTH`, `KEMTLS_MUTUAL`). ## State facts @@ -79,7 +80,7 @@ For KEMTLS, `stage` can be `'1'`, `'2'`, ..., `'6'`. - `!Pk(P, pk)`: Records that party `P`'s long-term public key is `pk`. - `!SessionKey(tid, stage, key)`: Records that the stage `stage` session key for thread `tid` is `key`. - `State(tid, mode, action, vars, transcript`: Records state for thread `tid` to be consumed by subsequent protocol actions. - - `mode` is the protocol mode the state is intended for (currently just `KEMTLS_SAUTH`). + - `mode` is the protocol mode the state is intended for. - `action` is the name of the protocol action that output this state (e.g., `ClientAction1`, `ClientAction2`, etc.) - `vars` is a tuple of variables (``). - `transcript` is a tuple of protocol messages. diff --git a/lemmas/reachable.spthy b/lemmas/reachable.spthy index 4d25588..36adf41 100644 --- a/lemmas/reachable.spthy +++ b/lemmas/reachable.spthy @@ -1,84 +1,24 @@ -lemma reachable_stage1: +define(,) +M_LEMMA_REACHABLE(KEMTLS_SAUTH, 1) +M_LEMMA_REACHABLE(KEMTLS_SAUTH, 2) +M_LEMMA_REACHABLE(KEMTLS_SAUTH, 3) +M_LEMMA_REACHABLE(KEMTLS_SAUTH, 4) +M_LEMMA_REACHABLE(KEMTLS_SAUTH, 5) +M_LEMMA_REACHABLE(KEMTLS_SAUTH, 6) diff --git a/protocol/kemtls_sauth_client.spthy b/protocol/kemtls_sauth_client.spthy index 921b0ea..0da458b 100644 --- a/protocol/kemtls_sauth_client.spthy +++ b/protocol/kemtls_sauth_client.spthy @@ -1,4 +1,3 @@ -// The client's first protocol action, generating an outgoing ephemeral KEM public key rule KEMTLS_SAUTH_ClientAction1: let pk_e = KEM_e_PK(~sk_e) @@ -13,14 +12,13 @@ rule KEMTLS_SAUTH_ClientAction1: Fr(~r_c) ] --[ - Owner(~tid, 'anonymous'), Role(~tid, 'client'), CID(~tid, '1', cid_1) ]-> [ Out(~tid), Out(), - State(~tid, 'KEMTLS_SAUTH', 'ClientAction1', <~sk_e, dES>, ) + State(~tid, 'KEMTLS_SAUTH_OR_MUTUAL', 'ClientAction1', <~sk_e, dES>, ) ] rule KEMTLS_SAUTH_ClientAction2: @@ -28,41 +26,43 @@ rule KEMTLS_SAUTH_ClientAction2: SERVER_HELLO = ss_e = KEM_e_Decaps(ct_e, sk_e) HS = HKDFExtract(dES, ss_e) - CHTS = HKDFExpand(HS, 'c_hs_traffic', ) - cid_1 = <'CHTS', CLIENT_HELLO, SERVER_HELLO> - sid_1 = <'CHTS', CLIENT_HELLO, SERVER_HELLO> - SHTS = HKDFExpand(HS, 's_hs_traffic', ) - cid_2 = <'SHTS', CLIENT_HELLO, SERVER_HELLO> - sid_2 = <'SHTS', CLIENT_HELLO, SERVER_HELLO> + CHTS = HKDFExpand(HS, 'c_hs_traffic', M_KEMTLS_SAUTH_STAGE1_TRANSCRIPT) + cid_1 = <'CHTS', M_KEMTLS_SAUTH_STAGE1_TRANSCRIPT> + sid_1 = <'CHTS', M_KEMTLS_SAUTH_STAGE1_TRANSCRIPT> + SHTS = HKDFExpand(HS, 's_hs_traffic', M_KEMTLS_SAUTH_STAGE1_TRANSCRIPT) + cid_2 = <'SHTS', M_KEMTLS_SAUTH_STAGE2_TRANSCRIPT> + sid_2 = <'SHTS', M_KEMTLS_SAUTH_STAGE2_TRANSCRIPT> dHS = HKDFExpand(HS, 'derived', '0') SERVER_CERTIFICATE = ct_S = KEM_s_Encaps_ct(pk_S, ~coins_S) ss_S = KEM_s_Encaps_ss(pk_S, ~coins_S) CLIENT_KEM_CIPHERTEXT = AHS = HKDFExtract(dHS, ss_S) - CAHTS = HKDFExpand(AHS, 'c_ahs_traffic', ) - cid_3 = <'CAHTS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT> - sid_3 = <'CAHTS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT> - SAHTS = HKDFExpand(AHS, 's_ahs_traffic', ) - cid_4 = <'SAHTS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT> - sid_4 = <'SAHTS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT> + CAHTS = HKDFExpand(AHS, 'c_ahs_traffic', M_KEMTLS_SAUTH_STAGE3_TRANSCRIPT) + cid_3 = <'CAHTS', M_KEMTLS_SAUTH_STAGE3_TRANSCRIPT> + sid_3 = <'CAHTS', M_KEMTLS_SAUTH_STAGE3_TRANSCRIPT> + SAHTS = HKDFExpand(AHS, 's_ahs_traffic', M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT) + cid_4 = <'SAHTS', M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT> + sid_4 = <'SAHTS', M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT> dAHS = HKDFExpand(AHS, 'derived', '0') MS = HKDFExtract(dAHS, '0') fk_c = HKDFExpand(MS, 'c_finished', '0') fk_s = HKDFExpand(MS, 's_finished', '0') - CF = HMAC(fk_c, ) + CF = HMAC(fk_c, M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT) CLIENT_FINISHED = - CATS = HKDFExpand(MS, 'c_ap_traffic', ) - cid_5 = <'CATS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED> - sid_5 = <'CATS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED> + CATS = HKDFExpand(MS, 'c_ap_traffic', M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT) + cid_5 = <'CATS', M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT> + sid_5 = <'CATS', M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT> in [ - State(tid, 'KEMTLS_SAUTH', 'ClientAction1', , ), + State(tid, 'KEMTLS_SAUTH_OR_MUTUAL', 'ClientAction1', , ), !Pk($S, pk_S), In(), Fr(~coins_S) ] --[ + ProtocolMode(tid, 'KEMTLS_SAUTH'), + Owner(tid, 'anonymous'), CID(tid, '1', cid_1), SID(tid, '1', sid_1), CID(tid, '2', cid_2), SID(tid, '2', sid_2), CID(tid, '3', cid_3), SID(tid, '3', sid_3), @@ -87,21 +87,21 @@ rule KEMTLS_SAUTH_ClientAction2: !SessionKey(tid, '4', SAHTS), !SessionKey(tid, '5', CATS), Out(), - State(tid, 'KEMTLS_SAUTH', 'ClientAction2', , ) + State(tid, 'KEMTLS_SAUTH', 'ClientAction2', , M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT) ] rule KEMTLS_SAUTH_ClientAction3: let SERVER_CERTIFICATE = - SF = HMAC(fk_s, ) + SF = HMAC(fk_s, M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT) SERVER_FINISHED = - SATS = HKDFExpand(MS, 's_ap_traffic', ) - cid_6 = <'SATS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED, SERVER_FINISHED> - sid_6 = <'SATS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED, SERVER_FINISHED> + SATS = HKDFExpand(MS, 's_ap_traffic', M_KEMTLS_SAUTH_STAGE6_TRANSCRIPT) + cid_6 = <'SATS', M_KEMTLS_SAUTH_STAGE6_TRANSCRIPT> + sid_6 = <'SATS', M_KEMTLS_SAUTH_STAGE6_TRANSCRIPT> in [ !Pk($S, pk_S), - State(tid, 'KEMTLS_SAUTH', 'ClientAction2', , ), + State(tid, 'KEMTLS_SAUTH', 'ClientAction2', , M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT), In() ] --[ diff --git a/protocol/kemtls_sauth_defines.spthy b/protocol/kemtls_sauth_defines.spthy new file mode 100644 index 0000000..e635ba1 --- /dev/null +++ b/protocol/kemtls_sauth_defines.spthy @@ -0,0 +1,7 @@ +define(,!>) +define(,!>) +define(,!>) +define(,!>) +define(,!>) +define(,!>) + diff --git a/protocol/kemtls_sauth_server.spthy b/protocol/kemtls_sauth_server.spthy index b2255dd..7382785 100644 --- a/protocol/kemtls_sauth_server.spthy +++ b/protocol/kemtls_sauth_server.spthy @@ -7,12 +7,12 @@ rule KEMTLS_SAUTH_ServerAction1: ES = HKDFExtract('0', '0') dES = HKDFExpand(ES, 'derived', '0') HS = HKDFExtract(dES, ss_e) - CHTS = HKDFExpand(HS, 'c_hs_traffic', ) - cid_1 = <'CHTS', CLIENT_HELLO, SERVER_HELLO> - sid_1 = <'CHTS', CLIENT_HELLO, SERVER_HELLO> - SHTS = HKDFExpand(HS, 's_hs_traffic', ) - cid_2 = <'SHTS', CLIENT_HELLO, SERVER_HELLO> - sid_2 = <'SHTS', CLIENT_HELLO, SERVER_HELLO> + CHTS = HKDFExpand(HS, 'c_hs_traffic', M_KEMTLS_SAUTH_STAGE1_TRANSCRIPT) + cid_1 = <'CHTS', M_KEMTLS_SAUTH_STAGE1_TRANSCRIPT> + sid_1 = <'CHTS', M_KEMTLS_SAUTH_STAGE1_TRANSCRIPT> + SHTS = HKDFExpand(HS, 's_hs_traffic', M_KEMTLS_SAUTH_STAGE2_TRANSCRIPT) + cid_2 = <'SHTS', M_KEMTLS_SAUTH_STAGE2_TRANSCRIPT> + sid_2 = <'SHTS', M_KEMTLS_SAUTH_STAGE2_TRANSCRIPT> dHS = HKDFExpand(HS, 'derived', '0') SERVER_CERTIFICATE = in @@ -24,6 +24,7 @@ rule KEMTLS_SAUTH_ServerAction1: Fr(~r_s) ] --[ + ProtocolMode(~tid, 'KEMTLS_SAUTH'), Owner(~tid, $S), Peer(~tid, 'anonymous'), Role(~tid, 'server'), @@ -48,12 +49,12 @@ rule KEMTLS_SAUTH_ServerAction2Part1: CLIENT_KEM_CIPHERTEXT = ss_S = KEM_s_Decaps(ct_S, sk_S) AHS = HKDFExtract(dHS, ss_S) - CAHTS = HKDFExpand(AHS, 'c_ahs_traffic', ) - cid_3 = <'CAHTS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT> - sid_3 = <'CAHTS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT> - SAHTS = HKDFExpand(AHS, 's_ahs_traffic', ) - cid_4 = <'SAHTS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT> - sid_4 = <'SAHTS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT> + CAHTS = HKDFExpand(AHS, 'c_ahs_traffic', M_KEMTLS_SAUTH_STAGE3_TRANSCRIPT) + cid_3 = <'CAHTS', M_KEMTLS_SAUTH_STAGE3_TRANSCRIPT> + sid_3 = <'CAHTS', M_KEMTLS_SAUTH_STAGE3_TRANSCRIPT> + SAHTS = HKDFExpand(AHS, 's_ahs_traffic', M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT) + cid_4 = <'SAHTS', M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT> + sid_4 = <'SAHTS', M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT> dAHS = HKDFExpand(AHS, 'derived', '0') in [ @@ -72,7 +73,7 @@ rule KEMTLS_SAUTH_ServerAction2Part1: [ !SessionKey(tid, '3', CAHTS), !SessionKey(tid, '4', SAHTS), - State(tid, 'KEMTLS_SAUTH', 'ServerAction2Part1', , ) + State(tid, 'KEMTLS_SAUTH', 'ServerAction2Part1', , M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT) ] rule KEMTLS_SAUTH_ServerAction2Part2: @@ -81,20 +82,20 @@ rule KEMTLS_SAUTH_ServerAction2Part2: MS = HKDFExtract(dAHS, '0') fk_c = HKDFExpand(MS, 'c_finished', '0') fk_s = HKDFExpand(MS, 's_finished', '0') - CF = HMAC(fk_c, ) + CF = HMAC(fk_c, M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT) CLIENT_FINISHED = - CATS = HKDFExpand(MS, 'c_ap_traffic', ) - cid_5 = <'CATS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED> - sid_5 = <'CATS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED> - SF = HMAC(fk_s, ) + CATS = HKDFExpand(MS, 'c_ap_traffic', M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT) + cid_5 = <'CATS', M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT> + sid_5 = <'CATS', M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT> + SF = HMAC(fk_s, M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT) SERVER_FINISHED = - SATS = HKDFExpand(MS, 's_ap_traffic', ) - cid_6 = <'SATS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED, SERVER_FINISHED> - sid_6 = <'SATS', CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED, SERVER_FINISHED> + SATS = HKDFExpand(MS, 's_ap_traffic', M_KEMTLS_SAUTH_STAGE6_TRANSCRIPT) + cid_6 = <'SATS', M_KEMTLS_SAUTH_STAGE6_TRANSCRIPT> + sid_6 = <'SATS', M_KEMTLS_SAUTH_STAGE6_TRANSCRIPT> in [ !Ltk($S, pk_S, sk_S), - State(tid, 'KEMTLS_SAUTH', 'ServerAction2Part1', , ), + State(tid, 'KEMTLS_SAUTH', 'ServerAction2Part1', , M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT), In() ] --[ @@ -110,4 +111,3 @@ rule KEMTLS_SAUTH_ServerAction2Part2: !SessionKey(tid, '6', SATS), Out() ] -