CCN protocol description and verification in Coq