We propose a framework for cyber risk assessment and mitigation which models attackers as formal planners and defenders as interdicting such plans. We illustrate the value of plan interdiction problems by first modeling network cyber risk through the use of formal planning, and subsequently formalizing an important question of prioritizing vulnerabilities for patching in the plan interdiction framework. In particular, we show that selectively patching relatively few vulnerabilities allows a network administrator to significantly reduce exposure to cyber risk. More broadly, we have developed a number of scalable approaches for plan interdiction problems, making especially significant advances when attack plans involve uncertainty about system dynamics. However, important open problems remain, including how to effectively capture information asymmetry between the attacker and defender, how to best model dynamics in the attacker-defender interaction, and how to develop scalable algorithms for solving associated plan interdiction games.