Polishing

README.md

@@ -1,7 +1,7 @@
 # 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/).
+The models were encoded for the [Tamarin model checker](https://tamarin-prover.github.io/), version 1.8.0.
 
 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.

proofs/Auxiliary.spthy

@@ -13,8 +13,6 @@ equations:
 
 
 
-heuristic: o "./oracle.py"
-
 restriction OnlyOnce:
   "∀ t #x #y. ((OnlyOnce( t ) @ #x) ∧ (OnlyOnce( t ) @ #y)) ⇒ (#x = #y)"
   // safety formula

signal-oidc.spthy

@@ -117,8 +117,6 @@ rule OIDCIdPIssueCode[color=#B4D9EF]:
   , TLSServer_In('GET', ~sess, $IdP, <'login', $Username, pw>) ]
   --[ IsCode(~code)
     , MustBeNonce(nonce)
-    // NOTE: It is not good that I make this annotation at the IdP. I must
-    // investigate this at a later point.
     , SOAPIdP($User, nonce, $IdP, $Username) ]->
   [ TLSClient_Out('GET', ~sess, $RedirectURL, <'code', ~code, nonce>)
   , St_OIDCIdP_Code($IdP, $Username, $Client, $RedirectURL, ~code, hash, nonce, code_challenge) ]