×

Formal verification of secure ad hoc routing protocols using AVISPA: ARAN case study. (English) Zbl 1231.68059

Grigoriu, Mircea (ed.) et al., European computing conference. Proceedings of the 4th European computing conference (ECC’10), Bucarest, Romania, April 20–22, 2010. Athens: World Scientific and Engineering Academy and Society (WSEAS) (ISBN 978-960-474-183-0/CD-ROM; 978-960-474-178-6/hbk). Electrical and Computer Engineering Series. A Series of Reference Books and Textbooks., 200-206 (2010).
Summary: Formal verification through model checking proved to be a very useful validation technique for security protocols: authentication, key agreement, non-repudiation, confidentiality, etc. But it has not been yet fully applied for the security properties of secure routing protocols for ad hoc networks. Few researchers had tried this approach but they had mainly used Promela and SPIN, a tool that is relatively difficult to use. On the other hand, other researchers used formal analysis, a mathematical approach with good results but which is hard to automate.
In this paper we present the use of AVISPA for this purpose. We show that the model under which the verification is made is identical to the models used by the researchers that implemented verification in SPIN or by the ones that used formal analysis. Then we present an actual verification taking as a case study ARAN secure routing protocol.
For the entire collection see [Zbl 1202.68005].

MSC:

68M12 Network protocols
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

HOL/SPIN
PDFBibTeX XMLCite