Home // International Journal On Advances in Security, volume 5, numbers 3 and 4, 2012 // View article

Verification with AVISPA to Engineer Network Security Protocols

Authors:
Florian Kammueller Florian Kammueller

Keywords: Security protocols, Model Checking, Crypto- graphic Hashes, Simple Protocol

Abstract:
This paper summarizes work on formal mecha- nized verification of security protocols using Avispa, a model checker dedicated to security protocols. Avispa has been successfully used in various Master’s projects. In this paper, we present two outstanding projects of quite different nature that highlight the spectrum of formal security protocol verification and lead us to a proposition of engineering practice for the development of secure protocols based on two main ideas (a) refactoring existing formalisations to prove adaptations of secu- rity protocols (b) compositional proof of new protocols allowing the combination and reuse of (parts of) existing formalisations of other protocols. This paper presents first Radius-SHA256, an adaptation of the Radius protocol for remote authentication for network access to the secure hash function SHA-256. Second, we present the Secure Simple Protocol which is an extension for security of a protocol developed at our university for next generation networks. Both protocols have been formalized in the Avispa model checker and security has been proved.

Pages: 112 to 120

Copyright: Copyright (c) to authors, 2012. Used with permission.

Publication date: December 31, 2012

Published in: journal

ISSN: 1942-2636