Formal verification of secure group communication protocols modelled in UML

Saqui-Sannes, Pierre de and Villemur, Thierry and Mota, Sara and Fontan, Benjamin and Bouassida, Mohamed Salah and Chridi, Najah and Chrisment, Isabelle and Vigneron, Laurent Formal verification of secure group communication protocols modelled in UML. (2010) Innovations in Systems and Software Engineering, 6 (1-2). 125-133. ISSN 1614-5046

Preview

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
688kB

Official URL: http://dx.doi.org/10.1007/s11334-010-0122-3

Abstract

The paper discusses an experience in using Unified Modelling Language and two complementary verification tools in the framework of SAFECAST, a project on secured group communication systems design. AVISPA enabled detecting and fixing security flaws. The TURTLE toolkit enabled saving development time by eliminating design solutions with inappropriate temporal parameters.

Item Type:	Article
Additional Information:	Second IEEE International workshop UML and Formal Methods - UML&FM'2009,Rio de Janeiro, 8 December 2008. Thanks to Springer editor. The definitive version is available at http://www.springerlink.com The original PDF of the article can be found at Innovations in Systems and Software Engineering website: http://www.springerlink.com/content/113014/
Audience (journal):	International peer-reviewed journal
Uncontrolled Keywords:	UML - Formal verification - Security - Real-time - Group protocols
Institution:	Other partners > Université de Franche-Comté (FRANCE) French research institutions > Institut National de la Recherche en Informatique et en Automatique - INRIA (FRANCE) French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE) Other partners > Institut National Polytechnique de Lorraine - INPL (FRANCE) Other partners > Université Henri Poincaré-Nancy1 - UHP (FRANCE) Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE) Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE) Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Laboratory name:	Département de Mathématiques, Informatique, Automatique - DMIA (Toulouse, France) - Modelisation et Architecture des Systèmes - MARS Laboratoire d'Analyse et d'Architecture des Systèmes - LAAS (Toulouse, France) - Outils Logiciels pour la Communication - OLC Laboratoire Lorrain de Recherche en Informatique et ses Applications - LORIA (Nancy, France) Heuristique et Diagnostic des Systèmes Complexes - HEUDIASYC (Compiègne, France)
Statistics:	download
Deposited On:	14 Apr 2010 06:42

Repository Staff Only: item control page