Merge remote-tracking branch 'upstream/develop' into free-equations

examples/loops/Minimal_HashChain.spthy

@@ -79,20 +79,25 @@ lemma Loop_charn [use_induction]:
   "All lid k kOrig #i. Loop(lid, k, kOrig) @ i ==>
      Ex #j. Loop(lid, kOrig, kOrig) @ j"
 
-// Not yet provable: the problem is that we cannot express the relation
-// between the keys on two different segments of the same loop.
-// @BS: Do you have an idea on how we could use multisets to formulate a
-// strong enough invariant?
-lemma Loop_and_success [use_induction]:
+lemma Helper_Loop_and_success[use_induction,reuse]:
+  "All lid kOrig k1 k2 #x #y #z.
+      Loop(lid, k1, kOrig) @ #x & Loop(lid, k2, kOrig) @ #y & #y < #x
+      & ChainKey(k1) @ #z
+    ==> Ex #t. ChainKey(k2) @ #t"
+
+lemma Loop_and_success:
   "All lid k kOrig1 kOrig2 #i #j.
        Loop(lid, k, kOrig1) @ i
      & Success(lid, kOrig2) @ j
     ==>
      (Ex #j. ChainKey(k) @ j)
   "
 
-// The ultimate goal! A successful check implies that the starting key is a
-// key of the chain.
+lemma Helper_Success_charn[use_induction,reuse]:
+  "All lid k kOrig #x #y.
+      ChainKey(k) @ #x & Loop(lid, k, kOrig) @ #y
+    ==> Ex #z. ChainKey(kOrig) @ #z"
+
 lemma Success_charn:
   "All lid k #i. Success(lid, k) @ i ==>
     Ex #j. ChainKey(k) @ j"

examples/usenix23-ens/README.md

@@ -0,0 +1,44 @@
+# Automated Security Analysis of Exposure Notification Systems
+
+## Authors
+
+- Kevin Morio, *CISPA Helmholtz Center for Information Security*
+- Ilkan Esiyok, *CISPA Helmholtz Center for Information Security*
+- Dennis Jackson, *Mozilla*
+- Robert Künnemann, *CISPA Helmholtz Center for Information Security*
+
+The paper has been accepted for *USENIX Security '23*.
+
+## Preprint
+
+A preprint of the full version of the paper is available on arXiv: [2210.00649](https://arxiv.org/abs/2210.00649)
+
+## Models
+
+### CWA (`cwa.spthy`)
+
+This is a model of a modified DP-3T design 1 following the CWA proposal with Google/Apple-style keys and authorisation scheme 3 (device bound authorisation).
+
+- Run as `tamarin-prover --prove cwa.spthy` in the terminal for automated mode,
+- Run as `tamarin-prover interactive cwa.spthy` for interactive mode.
+
+The oracle `oracle-cwa` is directly imported by the model.
+
+### DP3T (`dp3t.spthy`)
+
+This is a model of DP-3T design 3 with authorisation scheme 3 (device bound authorisation).
+
+- Run as `tamarin-prover --prove dp3t.spthy` in the terminal for automated mode,
+- Run as `tamarin-prover interactive dp3t.spthy` for interactive mode.
+
+The oracle `oracle-dp3t` is directly imported by the model.
+
+## ROBERT (`robert.spthy`)
+
+This is a model of ROBERT (ROBust and privacy-presERving proximity Tracing) / TousAntiCovid.
+
+- Run as `tamarin-prover --prove robert.spthy` in the terminal for automated mode,
+- Run as `tamarin-prover interactive robert.spthy` for interactive mode.
+
+The oracle `oracle-robert` is directly imported by the model.
+