Multiple long-term public key types

glossary.md

@@ -33,7 +33,13 @@ Accompanied by equational theory on correctness of decapsulation.
 
 All variants of KEMTLS can use:
 
-- `KEMTLS_KeyGen`:
+- `KEMTLS_KEM_s_KeyGen`:
+	- generates a new `KEM_s` key pair `(pk, sk)`
+	- binds a public key `pk` to a new party name `$P`
+	- outputs the public key
+
+- `KEMTLS_KEM_c_KeyGen`:
+	- generates a new `KEM_c` key pair `(pk, sk)`
 	- binds a public key `pk` to a new party name `$P`
 	- outputs the public key
 
@@ -60,7 +66,7 @@ All variants of KEMTLS can use:
 
 For KEMTLS, `stage` can be `'1'`, `'2'`, ..., `'6'`.
 
-- `Registered(P, pk)`: Records that a public key `pk` was registered for party `P`.
+- `Registered(P, pk, type)`: Records that a public key `pk` of type `type` (either `KEM_c` or `KEM_s`) was registered for party `P`.
 - `Owner(tid, P)` or `Owner(tid, 'anonymous')`: Records that the owner of thread `tid` is party `P` or is anonymous.
 - `Role(tid, 'client')` or `Role(tid, 'server')`: Records that the role of the party in thread `tid` is a client or a server.
 - `CID(tid, stage, cid)`: Records that the contributive identifier of stage `stage` for thread `tid` is `cid`.
@@ -76,8 +82,8 @@ For KEMTLS, `stage` can be `'1'`, `'2'`, ..., `'6'`.
 
 ## 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`.
+- `!Ltk(P, pk, sk, type)`: Records that party `P`'s long-term public key of type `type` is `pk` and the corresponding secret key is `sk`.
+- `!Pk(P, pk, type)`: Records that party `P`'s long-term public key of type `type` 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.
@@ -88,4 +94,4 @@ For KEMTLS, `stage` can be `'1'`, `'2'`, ..., `'6'`.
 ## Oracles
 
 - `ORevealSessionKey`: Reveals a session key recorded with `!SessionKey(tid, stage, key)`. Records this using a `RevealedSessionKey` action fact.
-- `OCorruptLTK`: Reveals the long-term secret key recorded with `!Ltk(P, pk, sk)`. Records this using a `Corrupted` action fact.
+- `OCorruptLTK`: Reveals the long-term secret key recorded with `!Ltk(P, pk, sk, type)`. Records this using a `Corrupted` action fact.

lemmas/malicious_acceptance.spthy

@@ -8,9 +8,9 @@ lemma malicious_acceptance:
     & Auth(tid, stage) @ #t_auth
     // (3) the peer's long-term key was not corrupted before the owner's stage was accepted as authenticated
     & not(
-      Ex S #tt1 #t_corrupted .
+      Ex S keytype #tt1 #t_corrupted .
       Peer(tid, S) @ #tt1
-      & CorruptedLTK(S) @ #t_corrupted
+      & CorruptedLTK(S, keytype) @ #t_corrupted
       & #t_corrupted < #t_auth
     )
     ==>

lemmas/sk_security.spthy

@@ -58,9 +58,9 @@ lemma sk_security_stage6_client_fs:
       // (5.b) the peer's long-term key was not corrupted before the owner's stage 6 accepted
       (
         not(
-          Ex S #tt1 #tt2 .
+          Ex S keytype #tt1 #tt2 .
           Peer(tid_c, S) @ #tt1
-          & CorruptedLTK(S) @ #tt2
+          & CorruptedLTK(S, keytype) @ #tt2
           & #tt2 < #tt1
         )
       )

model/oracles.spthy

@@ -13,10 +13,10 @@ rule ORevealSessionKey:
 // Oracle for revealing long-term keys
 rule OCorruptLTK:
   [
-    !Ltk($P, pk, sk)
+    !Ltk($P, pk, sk, type)
   ]
   --[
-    CorruptedLTK($P)
+    CorruptedLTK($P, type)
   ]->
   [
     Out(sk)

protocol/kemtls_keygen.spthy

@@ -1,16 +1,32 @@
-rule KEMTLS_KeyGen:
+rule KEMTLS_KEM_s_KeyGen:
   let 
     pk_P = KEM_s_PK(~sk_P)
   in
   [
     Fr(~sk_P)
   ]
   --[
-    RegisteredLTK($P, pk_P)
+    RegisteredLTK($P, pk_P, 'KEM_s')
   ]->
   [
-    !Ltk($P, pk_P, ~sk_P),
-    !Pk($P, pk_P),
+    !Ltk($P, pk_P, ~sk_P, 'KEM_s'),
+    !Pk($P, pk_P, 'KEM_s'),
     Out(pk_P)
   ]
 
+rule KEMTLS_KEM_c_KeyGen:
+let 
+  pk_P = KEM_c_PK(~sk_P)
+in
+[
+  Fr(~sk_P)
+]
+--[
+  RegisteredLTK($P, pk_P, 'KEM_c')
+]->
+[
+  !Ltk($P, pk_P, ~sk_P, 'KEM_c'),
+  !Pk($P, pk_P, 'KEM_c'),
+  Out(pk_P)
+]
+

protocol/kemtls_sauth_client.spthy

@@ -56,7 +56,7 @@ rule KEMTLS_SAUTH_ClientAction2:
   in
   [ 
     State(tid, 'KEMTLS_SAUTH_OR_MUTUAL', 'ClientAction1', <sk_e, dES>, <CLIENT_HELLO>), 
-    !Pk($S, pk_S),
+    !Pk($S, pk_S, 'KEM_s'),
     In(<SERVER_HELLO, SERVER_CERTIFICATE>), 
     Fr(~coins_S)
   ]
@@ -100,7 +100,7 @@ rule KEMTLS_SAUTH_ClientAction3:
     sid_6 = <'SATS', M_KEMTLS_SAUTH_STAGE6_TRANSCRIPT>
   in
   [
-    !Pk($S, pk_S),
+    !Pk($S, pk_S, 'KEM_s'),
     State(tid, 'KEMTLS_SAUTH', 'ClientAction2', <MS, fk_s>, M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT),
     In(<SERVER_FINISHED>)
   ]

protocol/kemtls_sauth_defines.spthy

@@ -4,4 +4,3 @@ define(<!M_KEMTLS_SAUTH_STAGE3_TRANSCRIPT!>,<!<CLIENT_HELLO, SERVER_HELLO, SERVE
 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>!>)
-

protocol/kemtls_sauth_server.spthy

@@ -18,7 +18,7 @@ rule KEMTLS_SAUTH_ServerAction1:
   in
   [
     Fr(~tid),
-    !Ltk($S, pk_S, sk_S),
+    !Ltk($S, pk_S, sk_S, 'KEM_s'),
     In(<CLIENT_HELLO>),
     Fr(~coins_e),
     Fr(~r_s)
@@ -58,7 +58,7 @@ rule KEMTLS_SAUTH_ServerAction2Part1:
     dAHS = HKDFExpand(AHS, 'derived', '0')
   in
   [
-    !Ltk($S, pk_S, sk_S),
+    !Ltk($S, pk_S, sk_S, 'KEM_s'),
     State(tid, 'KEMTLS_SAUTH', 'ServerAction1', <dHS>, <CLIENT_HELLO, SERVER_HELLO, SERVER_CERTIFICATE>),
     In(<CLIENT_KEM_CIPHERTEXT>)
   ]
@@ -78,7 +78,6 @@ rule KEMTLS_SAUTH_ServerAction2Part1:
 
 rule KEMTLS_SAUTH_ServerAction2Part2:
   let
-    SERVER_CERTIFICATE = <pk_S>
     MS = HKDFExtract(dAHS, '0')
     fk_c = HKDFExpand(MS, 'c_finished', '0')
     fk_s = HKDFExpand(MS, 's_finished', '0')
@@ -94,7 +93,6 @@ rule KEMTLS_SAUTH_ServerAction2Part2:
     sid_6 = <'SATS', M_KEMTLS_SAUTH_STAGE6_TRANSCRIPT>
   in
   [
-    !Ltk($S, pk_S, sk_S),
     State(tid, 'KEMTLS_SAUTH', 'ServerAction2Part1', <dAHS>, M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT),
     In(<CLIENT_FINISHED>)
   ]

protocol/primitives.spthy

@@ -1,13 +1,17 @@
 functions: 
   KEM_e_PK/1, KEM_e_Encaps_ct/2, KEM_e_Encaps_ss/2, KEM_e_Decaps/2,
   KEM_s_PK/1, KEM_s_Encaps_ct/2, KEM_s_Encaps_ss/2, KEM_s_Decaps/2,
+  KEM_c_PK/1, KEM_c_Encaps_ct/2, KEM_c_Encaps_ss/2, KEM_c_Decaps/2,
   HKDFExtract/2, HKDFExpand/3,
   HMAC/2
 
 equations:
   // correctness of KEM_e decapsulation
   KEM_e_Decaps(KEM_e_Encaps_ct(KEM_e_PK(sk), coins), sk) 
   = KEM_e_Encaps_ss(KEM_e_PK(sk), coins),
-  // correctness of KEM_e decapsulation
+  // correctness of KEM_s decapsulation
   KEM_s_Decaps(KEM_s_Encaps_ct(KEM_s_PK(sk), coins), sk) 
-  = KEM_s_Encaps_ss(KEM_s_PK(sk), coins)
+  = KEM_s_Encaps_ss(KEM_s_PK(sk), coins),
+  // correctness of KEM_c decapsulation
+  KEM_c_Decaps(KEM_c_Encaps_ct(KEM_c_PK(sk), coins), sk) 
+  = KEM_c_Encaps_ss(KEM_c_PK(sk), coins)