Formal Proof of Security Algorithms Based on Reachability Reduction
| Title | Formal Proof of Security Algorithms Based on Reachability Reduction |
| Publication Type | Conference Paper |
| Year of Publication | 2016 |
| Authors | Bouziane, Mohamed, Gire, Sophie, Monin, François, Nana, Laurent |
| Conference Name | Proceedings of the 8th International Conference on Management of Digital EcoSystems |
| Publisher | ACM |
| Conference Location | New York, NY, USA |
| ISBN Number | 978-1-4503-4267-4 |
| Keywords | attack graph, Attack Graphs, formal proof, Human Behavior, Identity management, identity snowball attack, Metrics, protocol verification, pubcrawl, reachability reduction, Resiliency, Scalability, security, sparsest\_cut |
| Abstract | 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. |
| URL | http://doi.acm.org/10.1145/3012071.3012085 |
| DOI | 10.1145/3012071.3012085 |
| Citation Key | bouziane_formal_2016 |