Game-theoretic approaches provide new ways to model and formally prove security properties of off-chain protocols. For complex protocols, carrying out such formal proofs is a cumbersome and error-prone task. We describe our ongoing efforts for automating the security analysis of off-chain protocols. We encode the game-theoretic protocol model, together with its security properties, as universally quantified formulas, and use SMT solving to enforce these properties.