EDHOC (Ephemeral Diffie-Hellman Over COSE) Symbolic Verification with ProVerif The model of the protocol should be run by: proverif edhoc_model_nocomment.pv