[sevenoftwelve]

Author of Rosenpass here;

Coq is fairly generic; it has a long history and made it possible to write some really cool proofs such as a proof of the four colors theorem, but writing crypto proofs is really hard using Coq.

For symbolic verification Tamarin and ProVerif are the tools of choice; I used ProVerif.

For proofs of security for protocols EasyCrypt and CryptoVerif can be used. CryptoVerif, ProVerif and Coq where developed at the same Institute by the way; at Inria Paris.