| Main objective |
The KLog project envisages to investigate and apply the tools and techniques of mathematical logic, in a broad sense, to the systematic study and design of special purpose classical and quantum kleistic (from the greek word kleisis) logics, that may provide a deeper understanding of the various aspects of information security, and ultimately contribute to the improvement of the available toolset of formal methods. This research will contribute to a better understanding of the relevant concepts and their relationships, and help to solve and clarify some of the open problems and key concerns of the area. The subjects to be addressed include the design and study of logics for reasoning about classical security protocols in distributed settings, ranging from the ideal world of perfect cryptography to the more realistic probabilistic setting where polynomially bounded adversaries are assumed, while also exploring type-theoretical logic systems targeted at flexible information flow analysis in languages supporting code mobility and declassification that could be used to express distributed protocols; and the logical study of quantum computation and information and its applications to security, eventually leading to quantum extensions of the logics for classical security, by considering quantum computation capabilities and quantum communication channels. The project will also not neglect the development of the logical foundations of combined logics and their algebraic counterparts motivated by the more applied research. Accordingly, the project is organized in three tasks: (T0) Logic in Computing; (T1) Logic for Classical Security; and (T2) Logic for Quantum Security.
|
