The widespread use of computers and internet in governance and
business requires the definition and implementation of adequate
security policies in accordance with international law.
The inclusion of a security policy in a computer system requires
a formal description of the policy that overcomes the ambiguities
that exist in natural language descriptions, and the development
of a formal framework that implements techniques to detect and
resolve conflicts and verify the correctness of the implemented
security protocols with respect to the given policy.
The aim of the project is first to explore different formal approaches
to security, in different areas such as access control, information
flow, cryptographic protocols, analysing case studies in different
application domains, and then to define a formal framework for the
specification and verification of both qualitative and quantitative
aspects of security, possibly integrating different approaches to
verification, such as model-checking and theorem-proving.