Maybe this answer is not quite in the spirit of your question, however the work "CryptHOL: Game-Based Proofs in Higher-Order Logic" (ref) and its implementation on AFP (ref) provide a framework for security proofs of cryptographic protocols, from its abstract:
Game-based proofs are a well-established paradigm for structuring security arguments and simplifying their understanding. We present a novel framework,
CryptHOL, for rigorous game-based proofs that is supported by mechanical theorem
proving. CryptHOL is based on a new semantic domain with an associated functional
programming language for expressing games. We embed our framework in the Isabelle/HOL theorem prover and, using the theory of relational parametricity, we tailor
Isabelle’s existing proof automation to game-based proofs. [..]
You can find a nice tutorial introduction here.
Since you mentioned Coq, there seems similar work going on in Coq: "SSProve: A Foundational Framework
for Modular Cryptographic Proofs in Coq" (ref)