The IDP system can be used to test the security and correctness of operational protocols, both for physical as well as information systems. Using logic, the different rules of the protocol can be modelled and a set of necessary guarantees can be stated (i.e., no outsider can get hold of private information).
Given these rules and the set of necessary guarantees, the IDP system can identify possible interactions between the different rules in the protocol that might result in breaches of the desired guarantees.
Information FlowIn this project, a formal approach to analyse privacy properties in complex electronic services is realized. A flexible framework for logic reasoning allows for formally modelling these services and inferring privacy properties that can be interpreted by the modeler. Therefore, the inference strategy consists of compiling user profiles according to the user's expectations in the data practices of all involved service providers. An example of an application within this context can be found here, and more information is available on the following github space.
Many systems, both in public service as in the private sector, have multiple ways of regulating its function, for example input sensors, controller software, and manual instruction (both on-site as online). These various methods interact in complex, sometimes unspecified ways. These interacting methods of control can cause many unintended security issues, certainly when some interactions are unspecified.
- Koen Decroix, Jorn Lapon, Bart De Decker, Vincent Naessens. "A Framework for Formal Reasoning about Privacy Properties Based on Trust Relationships in Complex Electronic Services." in Lecture Notes in Computer Science Volume 8303, pp 106-120, 2013. PDF