Security Proofs

[franziskuskiefer]

The goal is to prove handshake security properties for the code derived from TLS 1.3.
In particular, we will prove server authentication and session key secrecy.

• Generated model + small handwritten supplemental model should typecheck
• Minimize the number of functions that must be modeled by hand, goal: ~20 (current: 57)
• [ProVerif] Demonstrate the ProVerif model is working via reachability analysis #100
• [ProVerif] Remove unnecessary auto-generated events from model #104
  - [ProVerif] Insert handwritten model parts automatically instead of manual patching #105
  - [ProVerif] Incorporate code changes from Proving Panic Freedom in F* #112 into ProVerif model

[jschneider-bensch]

Moved the maintenance related task out of here.