First stage of PDK SAUTH or MUTUAL is not distinguished

kemtls · Jan 10, 2022 · 006588e · 006588e
1 parent 8bf497f
commit 006588e
Show file tree

Hide file tree

Showing 5 changed files with 6 additions and 6 deletions.
diff --git a/lemmas/reachable.spthy b/lemmas/reachable.spthy
@@ -129,7 +129,7 @@ M_LEMMA_REACHABLE(KEMTLS_MUTUAL, 6, 6, ⊤, ⊥, fs, fs, ⊥)
  * codification of the FS and auth parameters specified in Section B.3
  * of https://eprint.iacr.org/2021/779.pdf.
  */
-M_LEMMA_REACHABLE(KEMTLS_PDK_SAUTH, 1, 1, ⊥, ⊥, nofs, nofs, ⊤)
+M_LEMMA_REACHABLE(KEMTLS_PDK_SAUTH_OR_MUTUAL, 1, 1, ⊥, ⊥, nofs, nofs, ⊤)
 M_LEMMA_REACHABLE(KEMTLS_PDK_SAUTH, 1, 2, ⊥, ⊥, nofs, nofs, ⊤)
 M_LEMMA_REACHABLE(KEMTLS_PDK_SAUTH, 1, 3, ⊥, ⊥, nofs, nofs, ⊤)
 M_LEMMA_REACHABLE(KEMTLS_PDK_SAUTH, 1, 4, ⊤, ⊥, nofs, nofs, ⊤)
@@ -151,7 +151,7 @@ M_LEMMA_REACHABLE(KEMTLS_PDK_SAUTH, 5, 5, ⊥, ⊥, fs, wfs1, ⊥)
  * codification of the FS and auth parameters specified in Section B.3
  * of https://eprint.iacr.org/2021/779.pdf.
  */
-M_LEMMA_REACHABLE(KEMTLS_PDK_MUTUAL, 1, 1, ⊥, ⊥, nofs, nofs, ⊤)
+dnl M_LEMMA_REACHABLE(KEMTLS_PDK_MUTUAL, 1, 1, ⊥, ⊥, nofs, nofs, ⊤)
 M_LEMMA_REACHABLE(KEMTLS_PDK_MUTUAL, 1, 2, ⊥, ⊥, nofs, nofs, ⊤)
 M_LEMMA_REACHABLE(KEMTLS_PDK_MUTUAL, 1, 3, ⊥, ⊥, nofs, nofs, ⊤)
 M_LEMMA_REACHABLE(KEMTLS_PDK_MUTUAL, 1, 4, ⊤, ⊥, nofs, nofs, ⊤)

diff --git a/protocol/kemtls_pdk_mutual_client.spthy b/protocol/kemtls_pdk_mutual_client.spthy
@@ -22,7 +22,7 @@ rule KEMTLS_PDK_MUTUAL_ClientAction1:
   ]
   --[
     Role(~tid, 'client'),
-    ProtocolMode(~tid, '1', '1', 'KEMTLS_PDK_MUTUAL'),
+    ProtocolMode(~tid, '1', '1', 'KEMTLS_PDK_SAUTH_OR_MUTUAL'),
     CID(~tid, '1', cid_1), SID(~tid, '1', sid_1),
     Accept(~tid, '1'),
     Owner(~tid, $C),

diff --git a/protocol/kemtls_pdk_mutual_server.spthy b/protocol/kemtls_pdk_mutual_server.spthy
@@ -42,7 +42,7 @@ rule KEMTLS_PDK_MUTUAL_ServerAction1:
     Fr(~r_s)
   ]
   --[
-    ProtocolMode(~tid, '1', '1', 'KEMTLS_PDK_MUTUAL'),
+    ProtocolMode(~tid, '1', '1', 'KEMTLS_PDK_SAUTH_OR_MUTUAL'),
     ProtocolMode(~tid, '1', '2', 'KEMTLS_PDK_MUTUAL'),
     ProtocolMode(~tid, '1', '3', 'KEMTLS_PDK_MUTUAL'),
     ProtocolMode(~tid, '1', '4', 'KEMTLS_PDK_MUTUAL'),

diff --git a/protocol/kemtls_pdk_sauth_client.spthy b/protocol/kemtls_pdk_sauth_client.spthy
@@ -20,7 +20,7 @@ rule KEMTLS_PDK_SAUTH_ClientAction1:
   ]
   --[
     Role(~tid, 'client'),
-    ProtocolMode(~tid, '1', '1', 'KEMTLS_PDK_SAUTH'),
+    ProtocolMode(~tid, '1', '1', 'KEMTLS_PDK_SAUTH_OR_MUTUAL'),
     CID(~tid, '1', cid_1), SID(~tid, '1', sid_1),
     Accept(~tid, '1'),
     Owner(~tid, 'anonymous'),

diff --git a/protocol/kemtls_pdk_sauth_server.spthy b/protocol/kemtls_pdk_sauth_server.spthy
@@ -36,7 +36,7 @@ rule KEMTLS_PDK_SAUTH_ServerAction1:
     Fr(~r_s)
   ]
   --[
-    ProtocolMode(~tid, '1', '1', 'KEMTLS_PDK_SAUTH'),
+    ProtocolMode(~tid, '1', '1', 'KEMTLS_PDK_SAUTH_OR_MUTUAL'),
     ProtocolMode(~tid, '1', '2', 'KEMTLS_PDK_SAUTH'),
     ProtocolMode(~tid, '1', '3', 'KEMTLS_PDK_SAUTH'),
     ProtocolMode(~tid, '1', '4', 'KEMTLS_PDK_SAUTH'),