[PSQ] Model authenticated PSQ

[jschneider-bensch]

An authenticated version of the single-shot PSQ protocol.

[jschneider-bensch]

This is most of the way there, now. We hope we can strengthen one of the proven statements a little bit more.

[jschneider-bensch]

I've updated the model, so PQPSK_encaps will spit out the inner fresh value as well. This way we can show that ResponderGet(...) implies either InitiatorSend or the client was compromised and the attacker has access to the inner value (and thus the psk).

@karthikbhargavan: If you have time to check it out, please let me know if that closes this issue.