Formal analysis of security metrics and risk

Security metrics are usually defined informally and, therefore, the rigourous analysis of these metrics is a hard task. This analysis is required to identify the existing relations between the security metrics, which try to quantify the same quality: security. Risk, computed as Annualised Loss Expectancy, is often used in order to give the overall assessment of security as a whole. Risk and security metrics are usually defined separately and the relation between these indicators have not been considered thoroughly. In this work we fill this gap by providing a formal definition of risk and formal analysis of relations between security metrics and risk.