Update scripts and documentation to new proofs

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.

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 &

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` |

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