Update README

README.md

@@ -0,0 +1,18 @@
+# SOAP - Formal Proofs
+
+This repository contains the formal model and proofs for SOAP, a Social Authentication protocol.
+The models were encoded for the [Tamarin model checker](https://tamarin-prover.github.io/).
+
+As the model (`signal-oidc.spthy`) is very large and proofs take a considerable time (in the range of hours), the directory `/proofs` contains the finished proofs for every lemma in the theory.
+The README in that directory describes which proof-file contains proofs for which lemma.
+
+To check the proofs, first [install Tamarin](https://tamarin-prover.github.io/manual/book/002_installation.html).
+Afterwards, you can navigate to either the root folder or `/proofs` and run Tamarin in interactive mode:
+```
+tamarin-prover interactive .
+```
+
+Tamarin should then run on `localhost:3001`.
+If you navigate to that page, you should see a table showing one entry for every `*.spthy` file in the folder.
+Loading one of these files will also load the proofs.
+You can see that a lemma was proven if it is highlighted in green.

proofs/README.md

@@ -1,3 +1,21 @@
+## Proofs
+
+This directory contains all proofs for the model of SOAP.
+Note: there is a bug in tamarin that does not render every lemma green that has been verified.
+In particular, we experienced this for the executability lemma.
+To verify this lemma, you have to navigate to the leaf node of the proof tree that says "Constraint system solved".
+
+As the proofs can take a significant amount of time (the executability lemma can only be proven manually), we did not prove all lemmata in one file, and as such, have multiple proof files.
+The following table lists which source files contains proofs for which lemma.
+
+| Source file | Lemmata |
+| ----------- | --------|
+| `CodeVerifierSecrecy.spthy` | `CodeVerifierSecrecy` |
+| `Executability.spthy` | `Executability` |
+| `HelperLemmata.spthy` | `BrowserSessionSources`, `BrowserSessionBinding`, `BrowserSessionUnique`, `UsernamesUnique`, `UsernamesServerConfirmed`, `PasswordsConfidential`, `SignalKeysUnique`, `CodeIsSingleUse` |
+| `NonInjectiveAgreement.spthy` | `NonInjectiveAgreement` |
+| `SourcesLemma.spthy` | `TokenFormatAndOTPLearning` |
+
 ## Proof Complexity
 
 | Lemma | Steps |