Add some documentation and comments

README.md

@@ -0,0 +1,34 @@
+# Tamarain model for Core KEMTLS ("CoreKT")
+
+This repository contains a Tamarin model for the "core cryptographic version" of the KEMTLS protocol.  Roughly speaking, this means the version of KEMTLS as specified in Figures 3 and 7 of https://eprint.iacr.org/2020/534.pdf, without any additional the framing from the TLS protocol, such as extra TLS message fields, pre-shared key / resumption, or handshake / application layer encryption.
+
+The goal of this modelling exercise is to very closely follow the pen-and-paper security model and properties as specified in the multi-stage key exchange security model of the original paper (https://eprint.iacr.org/2020/534.pdf).
+
+## Organization of the code base
+
+- `glossary.md` summarizes the primitives, state facts, and action facts used throughout the protocol, model, and lemmas.
+
+- The `protocol` folder contains the formulation of the KEMTLS protocol in Tamarin.  In fact it includes two KEMTLS protocol modes: server-only authentication and mutual authentication.
+
+- The `model` folder contains oracles that are accessible to the adversary for compromising secret keys.
+
+- The `lemmas` folder contains lemmas modelling correctness and security properties.
+
+	- `lemmas/reachable.spthy` contains lemmas that model correctness of the protocol. In particular, we want to check that it is possible to generate sessions and stages that achieve each of the intended states.
+	- `lemmas/attacker_works.spthy` contains a few basic lemmas that check that it's possible for the attacker to trigger its various corruption queries.
+	- `lemmas/match_security.spthy` contains lemmas that model "match security". This means the sound behaviour of session matching: that, for honest sessions, the session identifier matches the partnered session. This is a codification of Section B.4 and Definition B.1 of https://eprint.iacr.org/2020/534.pdf. Please see Section B.4 of the paper for references on the origin of modelling match security as a separate property for authenticated key exchange protocols.
+	- `lemmas/sk_security.spthy` contains lemmas that model session key security. There are separate lemmas checking keys that are intended to have "weak forward secrecy 1", "weak forward secrecy 2", or "(full) forward secrecy".  This is a codification of the freshness conditions in Definition B.3 of https://eprint.iacr.org/2020/534.pdf.
+	- `lemmas/malicious_acceptance.spthy` contains a lemma authentication security of KEMTLS: for session stages that believe they have authenticated their peer, there really is a matching session. This is a codification of Definition B.4 in https://eprint.iacr.org/2020/534.pdf.
+
+- `corekt.spthy` uses m4 macros to pull all the above Tamarin source code into a single file.  Run the command `make preprocess` to generate the resulting file `generated_corekt.spthy`, which is the file you should actually have Tamarin run.
+
+- The `output` folder contains output from having run the model.
+
+## Getting started
+
+1. You'll need to have a working version of [Tamarin prover](https://tamarin-prover.github.io) installed.
+2. Run `make preprocess` to generate a single Tamarin file `generated_corekt.spthy` from all the above sources.
+3. Run `make prove` to have Tamarin try to prove all the above lemmas.  The output will be shown on the screen and stored in the `output` directory.  On a 16-core machine with lots of RAM, it takes about 7 minutes of wall clock time to prove all the lemmas.
+	- You can prove a specific lemma with `make prove PROVE=sk_securty_wfs1`
+	- You can also use the Tamarin web UI: `tamarin-prover interactive .`
+

glossary.md

@@ -100,6 +100,9 @@ All variants of KEMTLS can use:
 For KEMTLS, `stage` can be `'1'`, `'2'`, ..., `'6'`.
 
 - `Registered(P, pk, type)`: Records that a public key `pk` of type `type` (either `KEM_c` or `KEM_s`) was registered for party `P`.
+
+The following action facts directly correspond to variables in the multi stage key exchange model in Section B.1 of https://eprint.iacr.org/2020/534.pdf.
+
 - `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`.
@@ -109,9 +112,13 @@ For KEMTLS, `stage` can be `'1'`, `'2'`, ..., `'6'`.
 - `SK(tid, stage, key)`: Records that thread `tid` has accepted key `key` in stage `stage`.
 - `FS(tid, stage_target, stage_accepted, fslevel)`: Records that thread `tid` has during stage `stage_accepted` accepted the stage `stage_target` key as having forward secrecy level `fslevel` (in `wfs1`, `wfs2`, `fs`).
 - `Auth(tid, stage_target, stage_accepted)`: Records that thread `tid` has during stage `stage_accepted` accepted the stage `stage_target` key as authenticated.
+- `ProtocolMode(tid, stage_target, stage_accepted, mode)`: Records that thread `tid` has during stage `stage_accepted` accepted that stage `stage_target` was running in protocol mode `mode` (one of: `KEMTLS_SAUTH`, `KEMTLS_MUTUAL`, `KEMTLS_SAUTH_OR_MUTUAL`).
+	- Note this variable was not present in the original paper since the original model did not account for running multiple protocol modes simultaneously.
+
+The following action facts record adversary use of corruption oracles:
+
 - `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, stage_target, stage_accepted, mode)`: Records that thread `tid` has during stage `stage_accepted` accepted that stage `stage_target` was running in protocol mode `mode` (one of: `KEMTLS_SAUTH`, `KEMTLS_MUTUAL`, `KEMTLS_SAUTH_OR_MUTUAL`).
 
 ## State facts
 

lemmas/attacker_works.spthy

@@ -1,3 +1,10 @@
+/* This file contains a few basic lemmas that check that it's possible for the
+ * attacker to trigger its various corruption queries.
+ */
+
+/* This lemma checks that it is possible for the attacker to trigger the RevealSK 
+ * oracle.
+ */
 lemma attacker_works_revealsk:
   exists-trace
   "
@@ -6,6 +13,9 @@ lemma attacker_works_revealsk:
     RevealedSessionKey(tid, stage) @ #t1
   "
 
+/* This macro generates lemmas that check that it is possible for the attacker 
+ * to trigger the CorrupeLTK oracle for each type of long-term key.
+ */
 dnl M_LEMMA_ATTACKER_WORKS_CORRUPTLTK
 dnl arguments:
 dnl $1: KEM type (KEM_c, KEM_s)

lemmas/malicious_acceptance.spthy

@@ -1,18 +1,26 @@
+/* This lemma captures authentication security of KEMTLS: for session stages that 
+ * believe they have authenticated their peer (by recording Auth and Peer action 
+ * facts), there really is a matching session.
+ * This is a codification of Definition B.4 in https://eprint.iacr.org/2020/534.pdf.
+ * (Clauses numbered in parentheses (1), (2), (3) refer to clauses in Definition B.4 
+ * in the paper.)
+ */
 lemma malicious_acceptance:
   "
     All tid stage_target stage_accepted #t_accept #t_auth
     .
-    // the stage has accepted
+    // if the stage has accepted
     Accept(tid, stage_target) @ #t_accept
-    // (1) the stage has been accepted as authenticated (which may be later than when the stage accepted)
+    // and (1) the stage has been accepted as authenticated (which may be later than when the stage accepted)
     & Auth(tid, stage_target, stage_accepted) @ #t_auth
-    // (3) the peer's long-term key was not corrupted before the owner's stage was accepted as authenticated
+    // and (3) the peer's long-term key was not corrupted before the owner's stage was accepted as authenticated
     & not(
       Ex S keytype #tt1 #t_corrupted .
       Peer(tid, S) @ #tt1
       & CorruptedLTK(S, keytype) @ #t_corrupted
       & #t_corrupted < #t_auth
     )
+    // then
     ==>
       // there exists a partner at this stage
       (
@@ -21,7 +29,7 @@ lemma malicious_acceptance:
         & SID(tid, stage_target, sid) @ #tt1
         & SID(tid_other, stage_target, sid) @ #tt2
       )
-      // and it is unique (i.e., there are not three distinct instances with this sid)
+      // and (2) it is unique (i.e., there are not three distinct instances with this sid)
       & (
         not(
           Ex sid tid_1 tid_2 #tt0 #tt1 #tt2 .

lemmas/match_security.spthy

@@ -1,4 +1,19 @@
-lemma match_prop0: // extra property: they agree on protocol mode
+/* This file contains lemmas that model "match security". This means the sound 
+ * behaviour of session matching: that, for honest sessions, the session identifier 
+ * matches the partnered session. 
+ * This is a codification of Section B.4 and Definition B.1 of 
+ * https://eprint.iacr.org/2020/534.pdf.
+ */
+
+/* This lemma checks an extra match security property that isn't included in 
+ * Defintion B.1 of https://eprint.iacr.org/2020/534.pdf, but has been added here:
+ * if two sessions pi and pi' are partnered in some stage i (meaning that they 
+ * have pi.sid_i = pi'.sid_i), then they agree on which mode of KEMTLS they
+ * are using (sever-only authentication or mutual authentication).
+ * This condition was not included in the original paper because the model there
+ * did not consider simultaneous execution of multiple protocol modes.
+ */
+lemma match_prop0:
   "
     All tid_a tid_b stage_targeted stage_accepted sid mode_a mode_b #t1 #t2 #t3 #t4 #t5 #t6
     .
@@ -14,6 +29,15 @@ lemma match_prop0: // extra property: they agree on protocol mode
     )
   "
 
+/* This macro generates lemmas that check match security condition 1 as defined in 
+ * Defintion B.1 of https://eprint.iacr.org/2020/534.pdf.
+ * Match property 1 demands that, if two sessions pi and pi' are partnered in stage i
+ * (meaning that pi.sid_i = pi'.sid_i), then they agree the session key at all stages
+ * j ≤ i, i.e., pi.sk_j = pi'.sk_j for all j ≤ i.
+ * The lemma in the paper quantifies over all stages j ≤ i, but Tamarin does not
+ * let us model stages as integers that can be compared, so we use this macro to
+ * generate all possible (i, j) combinations satisfying j ≤ i, for i in {1, ..., 6}.
+ */
 define(<!M_LEMMA_PROP1!>,<!
 lemma match_prop1_i$1_j$2:
   "
@@ -49,6 +73,11 @@ M_LEMMA_PROP1(6, 4)
 M_LEMMA_PROP1(6, 5)
 M_LEMMA_PROP1(6, 6)
 
+/* This lemma checks match security condition 2 as defined in 
+ * Defintion B.1 of https://eprint.iacr.org/2020/534.pdf.
+ * Match property 2 demands that, if two sessions pi and pi' are partnered in some 
+ * stage i (meaning that pi.sid_i = pi'.sid_i), then they have opposite roles.
+ */
 lemma match_prop2:
   "
     All tid_a tid_b stage sid role_a role_b #t1 #t2 #t3 #t4
@@ -61,6 +90,12 @@ lemma match_prop2:
     ==> not(role_a = role_b)
   "
 
+/* This lemma checks match security condition 3 as defined in 
+ * Defintion B.1 of https://eprint.iacr.org/2020/534.pdf.
+ * Match property 3 demands that, if two sessions pi and pi' are partnered in some 
+ * stage i (meaning that they have the same *session* identifier pi.sid_i = pi'.sid_i), 
+ * then have also set and agree on the *contributive* identifier for that stage.
+ */
 lemma match_prop3:
   "
     All tid_a tid_b stage sid #t1 #t2
@@ -78,6 +113,14 @@ lemma match_prop3:
     )
   "
 
+/* This lemma checks match security condition 4 as defined in 
+ * Defintion B.1 of https://eprint.iacr.org/2020/534.pdf.
+ * Match property 4 demands that, if two sessions pi and pi' are partnered in some 
+ * stage i (meaning that they have pi.sid_i = pi'.sid_i), then for every stage 
+ * j ≤ i that has reached a (possibly retroactive) explicitly authenticated state.
+ * represented by setting Auth(..., stage_i), the identity of the peer is correct,
+ * i.e., that pi.peer = pi'.owner
+ */
 lemma match_prop4:
   "
     All tid_a tid_b stage_i stage_j sid A B #t1 #t2 #t3 #t4 #t5
@@ -91,6 +134,12 @@ lemma match_prop4:
     ==> A = B
   "
 
+/* This lemma checks match security condition 5 as defined in 
+ * Defintion B.1 of https://eprint.iacr.org/2020/534.pdf.
+ * Match property 5 demands that in any two (not necessarily)
+ * distinct sessions, distinct stages have distinct session identifiers,
+ * i.e., that pi.sid_i = pi''.sid_j implies i = j.
+ */
 lemma match_prop5:
   "
     All tid_a tid_b stage_i stage_j sid #t1 #t2
@@ -100,6 +149,13 @@ lemma match_prop5:
     ==> stage_i = stage_j
   "
 
+/* This lemma checks match security condition 6 as defined in 
+ * Defintion B.1 of https://eprint.iacr.org/2020/534.pdf.
+ * Match property 6 demands that, if two distinct sessions pi and pi' are partnered in some 
+ * stage i (meaning that they have pi.sid_i = pi'.sid_i), then there is no distinct
+ * third session that is also partnered in stage i (i.e., no pi'' != pi, pi' such that
+ * pi''.sid_i = pi.sid_i).
+ */
 lemma match_prop6:
   "
     All tid_a tid_b tid_c stage_i sid #t1 #t2 #t3

lemmas/reachable.spthy

@@ -1,3 +1,15 @@
+/* This file contains lemmas that model correctness of the protocol. In particular,
+ * we want to check that it is possible to generate sessions and stages that
+ * achieve each of the intended states.
+ */
+
+/* This macro generates lemmas that check that it is possible to reach a particular
+ * stage with the specified security properties.  A new lemma will be generated
+ * for each protocol mode (server-only authentication or mutual authentication),
+ * each stage we're retroactively assessing the properties of, the stage that
+ * has accepted, whether the client and server expect authentication at that stage,
+ * and what level of forward secrecy client and server expect at that stage.
+ */
 dnl M_LEMMA_REACHABLE
 dnl arguments:
 dnl $1: protocol mode (KEMTLS_MUTUAL, KEMTLS_SAUTH)
@@ -63,6 +75,14 @@ lemma reachable_$1_stage$2_accepted$3_c$6_s$7:
   "
 !>)
 
+// Now we apply the macro to generate the specific properties expected.
+
+/* For KEMTLS with server-only authentication, the lemmas below are a 
+ * codification of the FS and auth parameters specified in Section B.3
+ * of https://eprint.iacr.org/2020/534.pdf.
+ * Note that some protocol modes are marked as SAUTH_OR_MUTUAL because 
+ * the first few stages are the same in either mode.
+ */
 M_LEMMA_REACHABLE(KEMTLS_SAUTH_OR_MUTUAL, 1, 1, ⊥, ⊥, wfs1, wfs1)
 M_LEMMA_REACHABLE(KEMTLS_SAUTH, 1, 6, ⊤, ⊥, fs, wfs1)
 M_LEMMA_REACHABLE(KEMTLS_SAUTH_OR_MUTUAL, 2, 2, ⊥, ⊥, wfs1, wfs1)
@@ -75,13 +95,20 @@ M_LEMMA_REACHABLE(KEMTLS_SAUTH, 5, 5, ⊥, ⊥, wfs2, wfs1)
 M_LEMMA_REACHABLE(KEMTLS_SAUTH, 5, 6, ⊤, ⊥, fs, wfs1)
 M_LEMMA_REACHABLE(KEMTLS_SAUTH, 6, 6, ⊤, ⊥, fs, wfs1)
 
+/* For KEMTLS with mutual authentication, the lemmas below are a 
+ * codification of the FS and auth parameters specified in Section C.1
+ * of https://eprint.iacr.org/2020/534.pdf.
+ * Note that some protocol modes are marked as SAUTH_OR_MUTUAL because 
+ * the first few stages are the same in either mode; these are commented
+ * out here because they are the same as above.
+ */
 dnl M_LEMMA_REACHABLE(KEMTLS_SAUTH_OR_MUTUAL, 1, 1, ⊥, ⊥, wfs1, wfs1) dnl same as above
 M_LEMMA_REACHABLE(KEMTLS_MUTUAL, 1, 6, ⊤, ⊤, fs, fs)
 dnl M_LEMMA_REACHABLE(KEMTLS_SAUTH_OR_MUTUAL, 2, 2, ⊥, ⊥, wfs1, wfs1) dnl same as above
 M_LEMMA_REACHABLE(KEMTLS_MUTUAL, 2, 6, ⊤, ⊤, fs, fs)
-dnl M_LEMMA_REACHABLE(KEMTLS_SAUTH_OR_MUTUAL, 3, 3, ⊥, ⊥, wfs2, wfs2) dnl XXX different from paper
+dnl M_LEMMA_REACHABLE(KEMTLS_SAUTH_OR_MUTUAL, 3, 3, ⊥, ⊥, wfs2, wfs1) dnl same as above
 M_LEMMA_REACHABLE(KEMTLS_MUTUAL, 3, 6, ⊤, ⊤, fs, fs)
-dnl M_LEMMA_REACHABLE(KEMTLS_SAUTH_OR_MUTUAL, 4, 4, ⊥, ⊥, wfs2, wfs2) dnl XXX different from paper
+dnl M_LEMMA_REACHABLE(KEMTLS_SAUTH_OR_MUTUAL, 4, 4, ⊥, ⊥, wfs2, wfs1) dnl same as above
 M_LEMMA_REACHABLE(KEMTLS_MUTUAL, 4, 6, ⊤, ⊤, fs, fs)
 M_LEMMA_REACHABLE(KEMTLS_MUTUAL, 5, 5, ⊥, ⊤, wfs2, fs)
 M_LEMMA_REACHABLE(KEMTLS_MUTUAL, 5, 6, ⊤, ⊤, fs, fs)