A project of SQIG at IT, funded by FCT and EU FEDER PTDC/MAT/68723/2006 (October 1, 2007 - September 30, 2010).
Information security is an ancient concern of mankind, given its military, political, social, and economic implications. In this era of global electronic communication and commerce, it is no wonder that the subject is deserving increasing attention. When information and programs move throughout networks, they are exposed to users with different interests, goals and responsibilities. This motivates the search for practical mechanisms that enforce the respect for the desired security properties, while minimizing the need to rely on mutual trust. The security of information, communications, and systems in general, is thus one of the key scientific and technological challenges of the present, which has been attracting the attention of many mathematicians, logicians and computer scientists, over the past years. Due to the many subtleties that come into play, even in the simplest cryptographic protocols for secure communication (namely for electronic voting, commerce and contract signing, key exchange and authentication), it is now clear that the development of reliable security-critical applications must be supported by formal methods (read logics). This fact is well testified by the flaws found in several established protocols.
Despite of the advances obtained over the last years, the overall understanding of such a broad-spectrum area is still very shallow. In fact, it is widely recognized that only the joint understanding of a myriad of relevant phenomena like concurrency, communication, information flow, knowledge and belief, time and uncertainty, among others, can provide a realistic environment where secure systems and communication protocols may be specified and analysed, and where the intended security goals may be expressed and verified. Therefore, the area is quite interdisciplinary, requiring a deep understanding of algebra and number theory, information theory, computational complexity, and probability theory, concurrency and distribution. The plot has thickened even more with the emergence of the field of quantum computation and information triggered by the work of Shor in 1994, and its immediate security implications.
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.
For further information contact Carlos Caleiro (project coordinator).