%0 Journal Article %1 Pura10 %A Pura, Mihai-Lica %A Patriciu, Victor-Valeriu %A Bica, Ion %D 2010 %J Proceedings of the 4th European Computing Conference %K ARAN AVISPA routing secure formal verification %P 200-206 %T Formal verification of secure ad hoc routing protocols using AVISPA: ARAN case study %V 4

@article{Pura10, added-at = {2011-07-15T15:18:02.000+0200}, author = {Pura, Mihai-Lica and Patriciu, Victor-Valeriu and Bica, Ion}, biburl = {https://www.bibsonomy.org/bibtex/21a8fd0d94eef1db48d147aeda049605d/msteele}, file = {:I\:\\My Documents\\Thesis\\Research\\Pura10.pdf:PDF}, interhash = {841722d0d7c1c143847165bf3b41b8dd}, intrahash = {1a8fd0d94eef1db48d147aeda049605d}, journal = {Proceedings of the 4th European Computing Conference}, keywords = {ARAN AVISPA routing secure formal verification}, owner = {Matt}, pages = {200-206}, review = {AVISPA is a modeling and formal verification tool. It has similarities with SPIN. Results have only been obtained for no-intermediary node simulations. Attempts to run verification against 3 node networks have failed, consuming more than 72 hours of processing time. This is similar to the work presented in [<wibling04>] in which the all the modeling is attempted in the verifier itself. This lends support to the automated scripted style presented in [<andel07_b>]. AVISPA models are similar to SPIN models. Processes are the only first class structures. Time is not possible to be modeled. In all this is probably a very good start to modeling with AVISPA but it fails in the attempt to model everything in the verifier. AVISPA may be a valid alternative to SPIN and is worth a close look. Still don't know what AVISPA is though. Pura et. al. present the formal verification of ARAN with the AVISPA framework. AVISPA is similar to SPIN in that modeling is preformed through processes and there is no concept of time. [8] attempts to perform the entirety of the model checking in the verifier. This failed to produce results even for 3 node topologies. The failure to obtain results was caused by a state space explosion in the modeling. The claims that the use of the AVISPA framework is easier than SPIN so far have not panned out. More research is needed further explore the possibility of using AVISPA in formal routing verification.}, timestamp = {2011-07-15T19:53:10.000+0200}, title = {{Formal verification of secure ad hoc routing protocols using AVISPA: ARAN case study}}, volume = 4, year = 2010 }