diff --git a/README.md b/README.md
index f302517..bf7af7a 100644
--- a/README.md
+++ b/README.md
@@ -12,6 +12,8 @@ Afterwards, you can navigate to either the root folder or `/proofs` and run Tama
 tamarin-prover interactive .
 ```
 
+If you want to inspect the model for privacy, you must additionally provide the `--diff` argument to Tamarin.
+
 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.
diff --git a/batch-run-privacy.sh b/batch-run-privacy.sh
new file mode 100644
index 0000000..4401692
--- /dev/null
+++ b/batch-run-privacy.sh
@@ -0,0 +1 @@
+tamarin-prover-release --output=Privacy.spthy --prove=Observational_equivalence --diff signal-oidc-priv.spthy > Privacy.log 2>&1 &
diff --git a/proofs/README.md b/proofs/README.md
index ab2d1dc..ff51220 100644
--- a/proofs/README.md
+++ b/proofs/README.md
@@ -6,28 +6,13 @@ 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.
+The following table lists which source files contains proofs for which lemma in which model source file.
 
-| 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 |
-| ----- | ----- |
-| BrowserSessionSources | 10 |
-| BrowserSessionBinding | 55 |
-| BrowserSessionUnique | 10 |
-| UsernamesUnique | 6 |
-| UsernamesServerConfirmed | 20 |
-| PasswordsConfidential | 18 |
-| SignalKeysUnique | 6 |
-| CodeVerifierSecrecy | 27 |
-| TokenFormatAndOTPLearning | 10791 |
-| CodeIsSingleUse | 32 |
-| NonInjectiveAgreement | 128147 |
+| Source file | Lemmata | Model File |
+| ----------- | ------- | ---------- |
+| `CodeVerifierSecrecy.spthy` | `CodeVerifierSecrecy` | `signal-oidc.spthy` |
+| `Executability.spthy` | `Executability` | `signal-oidc.spthy` |
+| `HelperLemmata.spthy` | `BrowserSessionSources`, `BrowserSessionBinding`, `BrowserSessionUnique`, `UsernamesUnique`, `UsernamesServerConfirmed`, `PasswordsConfidential`, `SignalKeysUnique`, `IsPW`, `UserAccountRequiresSignUp`, `CodeIsSingleUse` | `signal-oidc.spthy` |
+| `SocialAuthentication.spthy` | `SocialAuthentication` | `signal-oidc.spthy` |
+| `SourcesLemma.spthy` | `TokenFormatAndOTPLearning` | `signal-oidc.spthy` |
+| `Privacy.spthy` | `Observational_equivalence` | `signal-oidc-priv.spthy` |
diff --git a/prove-all.sh b/prove-all.sh
index 77db355..0804e9a 100755
--- a/prove-all.sh
+++ b/prove-all.sh
@@ -2,3 +2,4 @@
 ./batch-run.sh CodeVerifierSecrecy --prove=CodeVerifierSecrecy
 ./batch-run.sh HelperLemmata --prove=BrowserSessionSources --prove=BrowserSessionBinding --prove=BrowserSessionUnique --prove=UsernamesUnique --prove=UsernamesServerConfirmed --prove=PasswordsConfidential --prove=SignalKeysUnique --prove=IsPW --prove=CodeIsSingleUse --prove=UserAccountRequiresSignUp
 ./batch-run.sh SourcesLemma --prove=TokenFormatAndOTPLearning
+./batch-run-privacy.sh