Use macros for transcripts

kemtls · Nov 4, 2021 · cd60bde · cd60bde
1 parent b2b5b56
commit cd60bde
Show file tree

Hide file tree

Showing 7 changed files with 80 additions and 126 deletions.
diff --git 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
@@ -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
@@ -72,14 +72,15 @@ 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
 
 - `!Ltk(P, pk, sk)`: Records that party `P`'s long-term public key is `pk` and the corresponding secret key is `sk`.
 - `!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 (`<var1, var2, etc>`).
 	- `transcript` is a tuple of protocol messages.

diff --git a/lemmas/reachable.spthy b/lemmas/reachable.spthy
@@ -1,84 +1,24 @@
-lemma reachable_stage1:
+define(<!M_LEMMA_REACHABLE!>,<!
+lemma reachable_$1_stage$2:
   exists-trace
   "
-    Ex tid_c tid_s sid #t1 #t2 #t3 #t4 #t5 #t6
+    Ex tid_c tid_s sid #t1 #t2 #t3 #t4 #t5 #t6 #t7 #t8
     .
-    Accept(tid_c, '1') @ #t1
-    & Accept(tid_s, '1') @ #t2
+    Accept(tid_c, '$2') @ #t1
+    & Accept(tid_s, '$2') @ #t2
     & Role(tid_c, 'client') @ #t3
     & Role(tid_s, 'server') @ #t4
-    & SID(tid_c, '1', sid) @ #t5
-    & SID(tid_s, '1', sid) @ #t6
-    & not(tid_c = tid_s)
-  "
-
-lemma reachable_stage2:
-  exists-trace
-  "
-    Ex tid_c tid_s sid #t1 #t2 #t3 #t4 #t5 #t6
-    .
-    Accept(tid_c, '2') @ #t1
-    & Accept(tid_s, '2') @ #t2
-    & Role(tid_c, 'client') @ #t3
-    & Role(tid_s, 'server') @ #t4
-    & SID(tid_c, '2', sid) @ #t5
-    & SID(tid_s, '2', sid) @ #t6
-    & not(tid_c = tid_s)
-  "
-
-lemma reachable_stage3:
-  exists-trace
-  "
-    Ex tid_c tid_s sid #t1 #t2 #t3 #t4 #t5 #t6
-    .
-    Accept(tid_c, '3') @ #t1
-    & Accept(tid_s, '3') @ #t2
-    & Role(tid_c, 'client') @ #t3
-    & Role(tid_s, 'server') @ #t4
-    & SID(tid_c, '3', sid) @ #t5
-    & SID(tid_s, '3', sid) @ #t6
-    & not(tid_c = tid_s)
-  "
-
-lemma reachable_stage4:
-  exists-trace
-  "
-    Ex tid_c tid_s sid #t1 #t2 #t3 #t4 #t5 #t6
-    .
-    Accept(tid_c, '4') @ #t1
-    & Accept(tid_s, '4') @ #t2
-    & Role(tid_c, 'client') @ #t3
-    & Role(tid_s, 'server') @ #t4
-    & SID(tid_c, '4', sid) @ #t5
-    & SID(tid_s, '4', sid) @ #t6
-    & not(tid_c = tid_s)
-  "
-
-lemma reachable_stage5:
-  exists-trace
-  "
-    Ex tid_c tid_s sid #t1 #t2 #t3 #t4 #t5 #t6
-    .
-    Accept(tid_c, '5') @ #t1
-    & Accept(tid_s, '5') @ #t2
-    & Role(tid_c, 'client') @ #t3
-    & Role(tid_s, 'server') @ #t4
-    & SID(tid_c, '5', sid) @ #t5
-    & SID(tid_s, '5', sid) @ #t6
-    & not(tid_c = tid_s)
-  "
-
-lemma reachable_stage6:
-  exists-trace
-  "
-    Ex tid_c tid_s sid #t1 #t2 #t3 #t4 #t5 #t6
-    .
-    Accept(tid_c, '6') @ #t1
-    & Accept(tid_s, '6') @ #t2
-    & Role(tid_c, 'client') @ #t3
-    & Role(tid_s, 'server') @ #t4
-    & SID(tid_c, '6', sid) @ #t5
-    & SID(tid_s, '6', sid) @ #t6
+    & SID(tid_c, '$2', sid) @ #t5
+    & SID(tid_s, '$2', sid) @ #t6
+    & ProtocolMode(tid_c, '$1') @ #t7
+    & ProtocolMode(tid_s, '$1') @ #t8
     & not(tid_c = tid_s)
   "
+!>)
 
+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
@@ -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,56 +12,57 @@ rule KEMTLS_SAUTH_ClientAction1:
     Fr(~r_c)
   ]
   --[
-    Owner(~tid, 'anonymous'),
     Role(~tid, 'client'),
     CID(~tid, '1', cid_1)
   ]->
   [
     Out(~tid),
     Out(<CLIENT_HELLO>),
-    State(~tid, 'KEMTLS_SAUTH', 'ClientAction1', <~sk_e, dES>, <CLIENT_HELLO>)
+    State(~tid, 'KEMTLS_SAUTH_OR_MUTUAL', 'ClientAction1', <~sk_e, dES>, <CLIENT_HELLO>)
   ]
 
 rule KEMTLS_SAUTH_ClientAction2:
   let
     SERVER_HELLO = <ct_e, r_s>
     ss_e = KEM_e_Decaps(ct_e, sk_e)
     HS = HKDFExtract(dES, ss_e)
-    CHTS = HKDFExpand(HS, 'c_hs_traffic', <CLIENT_HELLO, SERVER_HELLO>)
-    cid_1 = <'CHTS', CLIENT_HELLO, SERVER_HELLO>
-    sid_1 = <'CHTS', CLIENT_HELLO, SERVER_HELLO>
-    SHTS = HKDFExpand(HS, 's_hs_traffic', <CLIENT_HELLO, SERVER_HELLO>)
-    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 = <pk_S>
     ct_S = KEM_s_Encaps_ct(pk_S, ~coins_S)
     ss_S = KEM_s_Encaps_ss(pk_S, ~coins_S)
     CLIENT_KEM_CIPHERTEXT = <ct_S>
     AHS = HKDFExtract(dHS, ss_S)
-    CAHTS = HKDFExpand(AHS, 'c_ahs_traffic', <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT>)
-    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', <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT>)
-    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, <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT>)
+    CF = HMAC(fk_c, M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT)
     CLIENT_FINISHED = <CF>
-    CATS = HKDFExpand(MS, 'c_ap_traffic', <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED>)
-    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', <sk_e, dES>, <CLIENT_HELLO>), 
+    State(tid, 'KEMTLS_SAUTH_OR_MUTUAL', 'ClientAction1', <sk_e, dES>, <CLIENT_HELLO>), 
     !Pk($S, pk_S),
     In(<SERVER_HELLO, SERVER_CERTIFICATE>), 
     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(<CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED>),
-    State(tid, 'KEMTLS_SAUTH', 'ClientAction2', <MS, fk_s>, <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED>)
+    State(tid, 'KEMTLS_SAUTH', 'ClientAction2', <MS, fk_s>, M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT)
   ]
 
 rule KEMTLS_SAUTH_ClientAction3:
   let
     SERVER_CERTIFICATE = <pk_S>
-    SF = HMAC(fk_s, <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED>)
+    SF = HMAC(fk_s, M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT)
     SERVER_FINISHED = <SF>
-    SATS = HKDFExpand(MS, 's_ap_traffic', <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED, SERVER_FINISHED>)
-    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', <MS, fk_s>, <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED>),
+    State(tid, 'KEMTLS_SAUTH', 'ClientAction2', <MS, fk_s>, M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT),
     In(<SERVER_FINISHED>)
   ]
   --[

diff --git a/protocol/kemtls_sauth_defines.spthy b/protocol/kemtls_sauth_defines.spthy
@@ -0,0 +1,7 @@
+define(<!M_KEMTLS_SAUTH_STAGE1_TRANSCRIPT!>,<!<CLIENT_HELLO, SERVER_HELLO>!>)
+define(<!M_KEMTLS_SAUTH_STAGE2_TRANSCRIPT!>,<!<CLIENT_HELLO, SERVER_HELLO>!>)
+define(<!M_KEMTLS_SAUTH_STAGE3_TRANSCRIPT!>,<!<CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT>!>)
+define(<!M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT!>,<!<CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT>!>)
+define(<!M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT!>,<!<CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED>!>)
+define(<!M_KEMTLS_SAUTH_STAGE6_TRANSCRIPT!>,<!<CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED, SERVER_FINISHED>!>)
+
diff --git 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', <CLIENT_HELLO, SERVER_HELLO>)
-    cid_1 = <'CHTS', CLIENT_HELLO, SERVER_HELLO>
-    sid_1 = <'CHTS', CLIENT_HELLO, SERVER_HELLO>
-    SHTS = HKDFExpand(HS, 's_hs_traffic', <CLIENT_HELLO, SERVER_HELLO>)
-    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 = <pk_S>
   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 = <ct_S>
     ss_S = KEM_s_Decaps(ct_S, sk_S)
     AHS = HKDFExtract(dHS, ss_S)
-    CAHTS = HKDFExpand(AHS, 'c_ahs_traffic', <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT>)
-    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', <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT>)
-    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', <dAHS>, <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT>)
+    State(tid, 'KEMTLS_SAUTH', 'ServerAction2Part1', <dAHS>, 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, <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT>)
+    CF = HMAC(fk_c, M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT)
     CLIENT_FINISHED = <CF>
-    CATS = HKDFExpand(MS, 'c_ap_traffic', <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED>)
-    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, <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>
+    SF = HMAC(fk_s, M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT)
     SERVER_FINISHED = <SF>
-    SATS = HKDFExpand(MS, 's_ap_traffic', <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_FINISHED, SERVER_FINISHED>)
-    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', <dAHS>, <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT>),
+    State(tid, 'KEMTLS_SAUTH', 'ServerAction2Part1', <dAHS>, M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT),
     In(<CLIENT_FINISHED>)
   ]
   --[
@@ -110,4 +111,3 @@ rule KEMTLS_SAUTH_ServerAction2Part2:
     !SessionKey(tid, '6', SATS),
     Out(<SERVER_FINISHED>)
   ]
-