Proper EC point validation

[malishav]

A PR on draft-ietf-lake-traces adds several invalid test vectors. Some of these contain messages with invalid G_X. In edhoc-rs, the point is not properly validated before the ECDH operation. This issue aims at adding point validation in process_message_1 and process_message_2 routines, which if failed, should return an error.

[chrysn]

When we do this, we may want to distinguish in the type system between "this is a buffer that holds a potential public key" and "this is a buffer that holds a valid public key".

[chrysn]

Proving freedom of panics (as I understand is one thing the hax converted thing can do) will be a tall order: It'll mean that the proof tool will need to remember that the only way to ever construct a public key is through the check at construction time, and that the branch that will later go from "this needs to be a valid point" to "otherwise I'll panic" will need to somehow match that knowledge.

Which, conversely, would allow incredibly defensive programming if the output of the proof could somehow be used on the Rust optimizer side to show that because there is proof of the property, the calculation doesn't have to be done again. Are there any plans to use that knowledge?