Abstract. Given the presence of residual vulnerabilities in software systems, it is critical to apply suitable countermeasures in order to minimize the likelihood of an attack. In this paper we propose a formal approach, based on stochastic games, to threat analysis and synthesis of defence strategies for protecting systems with vulnerabilities. Crucially, we support analysis under partial observation, where some of the attacker's activities are unobservable or undetectable by the defender. We construct a one-sided partially observable security game and transform it into a perfect game, for which formal analysis is feasible. We prove that this transformation is sound for a sub-class of security games and a subset of objectives specified in the temporal logic rPATL. We implement our approach and evaluate it by applying it to a real-life example.