How to express the existence of winning strategy of the starter of a game in temporal logic?

Question

Consider a two-player game. A winning strategy of a player is a strategy following which the player can always beat his opponent, no matter how his opponent responds.

A game can be unfolded to a state space consisting of the possible ways of both sides of the game. How to express the existence of winning strategy of the starter of a game, say player 1, in temporal logic, defined on such a state space? The temporal logic formula can be used for model checking.

Using CTL, I get $\exists \Box (\exists \Diamond \textsf{Win}_1)$, meaning that there exists a path (from the initial state) such that from each state of this path there exists a path that eventually leads to a winning state for player 1. Is this correct?

Can it be expressed in LTL or any other variants of temporal logic?