Biblio
Filters: Author is Monin, François [Clear All Filters]
.
2016. Formal Proof of Security Algorithms Based on Reachability Reduction. Proceedings of the 8th International Conference on Management of Digital EcoSystems. :67–72.
This work is motivated by the rapid increase of the number of attacks in computer networks and software engineering. In this paper we study identity snowball attacks and formally prove the correctness of suggested solutions to this type of attack (solutions that are based on the graph reachability reduction) using a proof assistant. We propose a model of an attack graph that captures technical informations about the calculation of reachability of the graph. The model has been implemented with the proof assistant PVS 6.0 (Prototype Verification System). It makes it possible to prove algorithms of reachability reduction such as Sparsest\_cut.