From 25a9a3aa4b4a7b1d8084e24e0ace4046775a3e15 Mon Sep 17 00:00:00 2001 From: Douglas Stebila Date: Thu, 4 Nov 2021 13:00:15 -0400 Subject: [PATCH] Multiple long-term public key types --- glossary.md | 16 +++++++++++----- lemmas/malicious_acceptance.spthy | 4 ++-- lemmas/sk_security.spthy | 4 ++-- model/oracles.spthy | 4 ++-- protocol/kemtls_keygen.spthy | 24 ++++++++++++++++++++---- protocol/kemtls_sauth_client.spthy | 4 ++-- protocol/kemtls_sauth_defines.spthy | 1 - protocol/kemtls_sauth_server.spthy | 6 ++---- protocol/primitives.spthy | 8 ++++++-- 9 files changed, 47 insertions(+), 24 deletions(-) diff --git a/glossary.md b/glossary.md index 444f795..f2978c9 100644 --- a/glossary.md +++ b/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. diff --git a/lemmas/malicious_acceptance.spthy b/lemmas/malicious_acceptance.spthy index df2fa4e..6113e39 100644 --- a/lemmas/malicious_acceptance.spthy +++ b/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 ) ==> diff --git a/lemmas/sk_security.spthy b/lemmas/sk_security.spthy index 95c0152..016e7ef 100644 --- a/lemmas/sk_security.spthy +++ b/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 ) ) diff --git a/model/oracles.spthy b/model/oracles.spthy index e89ca27..050e45e 100644 --- a/model/oracles.spthy +++ b/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) diff --git a/protocol/kemtls_keygen.spthy b/protocol/kemtls_keygen.spthy index 1e2d4e9..61c8ae1 100644 --- a/protocol/kemtls_keygen.spthy +++ b/protocol/kemtls_keygen.spthy @@ -1,4 +1,4 @@ -rule KEMTLS_KeyGen: +rule KEMTLS_KEM_s_KeyGen: let pk_P = KEM_s_PK(~sk_P) in @@ -6,11 +6,27 @@ rule KEMTLS_KeyGen: 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) +] + diff --git a/protocol/kemtls_sauth_client.spthy b/protocol/kemtls_sauth_client.spthy index 0da458b..78bdf58 100644 --- a/protocol/kemtls_sauth_client.spthy +++ b/protocol/kemtls_sauth_client.spthy @@ -56,7 +56,7 @@ rule KEMTLS_SAUTH_ClientAction2: in [ State(tid, 'KEMTLS_SAUTH_OR_MUTUAL', 'ClientAction1', , ), - !Pk($S, pk_S), + !Pk($S, pk_S, 'KEM_s'), In(), 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', , M_KEMTLS_SAUTH_STAGE5_TRANSCRIPT), In() ] diff --git a/protocol/kemtls_sauth_defines.spthy b/protocol/kemtls_sauth_defines.spthy index e635ba1..d10eac4 100644 --- a/protocol/kemtls_sauth_defines.spthy +++ b/protocol/kemtls_sauth_defines.spthy @@ -4,4 +4,3 @@ define(,,!>) define(,!>) define(,!>) - diff --git a/protocol/kemtls_sauth_server.spthy b/protocol/kemtls_sauth_server.spthy index 7382785..2f13f41 100644 --- a/protocol/kemtls_sauth_server.spthy +++ b/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(), 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', , ), In() ] @@ -78,7 +78,6 @@ rule KEMTLS_SAUTH_ServerAction2Part1: rule KEMTLS_SAUTH_ServerAction2Part2: let - SERVER_CERTIFICATE = 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', , M_KEMTLS_SAUTH_STAGE4_TRANSCRIPT), In() ] diff --git a/protocol/primitives.spthy b/protocol/primitives.spthy index c541504..871540c 100644 --- a/protocol/primitives.spthy +++ b/protocol/primitives.spthy @@ -1,6 +1,7 @@ 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 @@ -8,6 +9,9 @@ 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)