LOCKS: a property specification language for security goals

We introduce a formal specification language LOCKS, that allow security practitioners to express as well as compose security goals in a convenient manner. LOCKS supports the specification of the most common security properties over generic attributes, both for qualitative and quantitative goals. To make our language independent of a specific security framework, we evaluate LOCKS over a generic attack model, namely the structural attack model (SAM), which over-arches the most prominent graphical threat models. Furthermore, we equip our language with a concise grammar, type rules and denotational semantics, thus laying the foundations of an automated tool. We take a number of informal security goals from the literature and show how they can be formally expressed in our language.