As using the ProVerif to verify the correctness of any security protocol we simulate the protocol and its environment (what an attacker knows and what he can know), so why do we need to check old protocols? And why have these not been checked (verified) after development, before being used?
thanks alot Mr. Sebastian Banescu.
I'm still new to this field, and i want to take my master thesis into this area.
But i mean, the overall process is a simulation to protocol we want verify and its environment (what the attacker know and he can know), and because it is just a simulation, how can checking old protocols lead to new attacks (why these attacks have not been discovered early, at first verification? ), and why Needham–Schroeder protocol was not discovered to be vulnerable in 1978 ?
Best regards.
In addition to Sebastian's comment I would like to point out that not everything can be verified by tools like proverif or scyther. Especially problematic are broadcast networks, time-critical systems and systems that operate on data rather than on abstracted packets.
A (somewhat) practical example:
Data aggregation in mobile ad-hoc networks. In such a scenario, many small nodes are distributed in a location (e.g. a tunnel) to monitor for a specific property (say, temperature). An attacker may compromise a subset of these nodes to falsely represent the data. As it is not cost-effectively possible to protect all nodes with hardware security modules, we use protocols and very large amounts of nodes to protect the integrity of the data. However, we also aggregate within the network (because sending messages costs significant power) to save bandwidth. Our goal is then to minimize the impact of an attacker - but it is very difficult to provide guarantees or bounds on the potential impact of an attack.
- Badges
- Science topic