JACOMME Charlie authored May 14, 2024 and BLANCHET Bruno committed May 14, 2024

Merge of branch crypto-library-pq-version

- Library of primitives:
   - added macros for primitives without security assumption (useful
   to model broken primitives; e.g., classical schemes in the presence of
   a quantum adversary).
   - added macros for IND-CPA public key encryption, KEMs
   (Key Encapsulation Mechanisms), and fixed-hash collision-resistant hash
   functions. (The latter make sense only against a fixed adversary.)
   - built a separate library for assumptions valid against a quantum
   adversary (pq.cvl, pq.ocvl).
- Models for pq-ssh and pq-tls
- Fixed notion of key exchange for SSH
- Proof of HPKE base mode from KEM and DHKEM in base mode; cleanup
  in HPKE models

Co-authored-by: Bruno Blanchet <Bruno.Blanchet@inria.fr>