Jonas/coprf pv

[jschneider-bensch]

Regarding reachability.pv:

• I can see why LakeReceived(...) ==> SourceSent(...) might be false, since after changing the top-level process such that the attacker can input directly to all parties, the attacker could just play the role of an honest DataSource itself.
• I'm not sure, however, why even LakeReceived(...) on its own cannot be proved.

Regarding pseudonymity.pv:

• Leaking the blinding secret key bsk allows the attacker to compare the generated pseudonym (a value of the form prf(derive_key(...),uid)) to what the attacker expects from a previous conversion of the same uid (?).
• I think what we want to show is a real-or-random property something like: given real input (uid, attribute_1, attribute_2) the processed output (pseudonym_1, pseudonym_2) where pseudonym_{1,2} are honestly generated should be indistinguishable from output (pseudonym_1, pseudonym_$) where pseudonym_$ is a fresh value.

[franziskuskiefer]

@karthikbhargavan please do a review