UML Modeling and Formal Verification of Secure Group Communication Protocols

Pierre De Saqui-Sannes; Thierry Villemur; Benjamin Fontan; Sara Mota; Mohamed Salah Bouassida; Najah Chridi; Isabelle Chrisment; Laurent Vigneron

hal-00447668, version 1

UML Modeling and Formal Verification of Secure Group Communication Protocols

Pierre De Saqui-Sannes ¹, Thierry Villemur ¹, Benjamin Fontan ¹, Sara Mota ¹, Mohamed Salah Bouassida () ², Najah Chridi ³, Isabelle Chrisment () ⁴, Laurent Vigneron () ³

Second IEEE International workshop UML and Formal Methods - UML&FM'2009 (2009) --

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

1: Laboratoire d'analyse et d'architecture des systèmes (LAAS)
CNRS : UPR8001 – Université Paul Sabatier [UPS] - Toulouse III – Institut National Polytechnique de Toulouse - INPT – Institut National des Sciences Appliquées (INSA) - Toulouse
2: Heuristique et Diagnostic des Systèmes Complexes (HEUDIASYC)
CNRS : UMR6599 – Université de Technologie de Compiègne
3: CASSIS (INRIA Lorraine - LORIA / LIFC)
INRIA – CNRS : FRE2661 – Université de Franche-Comté – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
4: MADYNES (INRIA Lorraine - LORIA)
INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)

hal-00447668, version 1
http://hal.archives-ouvertes.fr/hal-00447668
oai:hal.archives-ouvertes.fr:hal-00447668
From: Mohamed Salah Bouassida <>
Submitted on: Friday, 15 January 2010 15:28:26
Updated on: Wednesday, 27 January 2010 09:29:40

See detailed view

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="hal-00447668"><analytic>
<author><persName><forename>Pierre</forename><surname>De Saqui-Sannes</surname></persName>
<affiliation>
<orgName type="laboratory">LAAS</orgName>
<orgName type="team">Laboratoire d'analyse et d'architecture des systèmes</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UPR8001</orgName>
<orgName type="institution">Université Paul Sabatier [UPS] - Toulouse III</orgName>
<orgName type="institution">Institut National Polytechnique de Toulouse - INPT</orgName>
<orgName type="institution">Institut National des Sciences Appliquées (INSA) - Toulouse</orgName>
</affiliation>
</author>
<author><persName><forename>Thierry</forename><surname>Villemur</surname></persName>
<affiliation>
<orgName type="laboratory">LAAS</orgName>
<orgName type="team">Laboratoire d'analyse et d'architecture des systèmes</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UPR8001</orgName>
<orgName type="institution">Université Paul Sabatier [UPS] - Toulouse III</orgName>
<orgName type="institution">Institut National Polytechnique de Toulouse - INPT</orgName>
<orgName type="institution">Institut National des Sciences Appliquées (INSA) - Toulouse</orgName>
</affiliation>
</author>
<author><persName><forename>Benjamin</forename><surname>Fontan</surname></persName>
<affiliation>
<orgName type="laboratory">LAAS</orgName>
<orgName type="team">Laboratoire d'analyse et d'architecture des systèmes</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UPR8001</orgName>
<orgName type="institution">Université Paul Sabatier [UPS] - Toulouse III</orgName>
<orgName type="institution">Institut National Polytechnique de Toulouse - INPT</orgName>
<orgName type="institution">Institut National des Sciences Appliquées (INSA) - Toulouse</orgName>
</affiliation>
</author>
<author><persName><forename>Sara</forename><surname>Mota</surname></persName>
<affiliation>
<orgName type="laboratory">LAAS</orgName>
<orgName type="team">Laboratoire d'analyse et d'architecture des systèmes</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UPR8001</orgName>
<orgName type="institution">Université Paul Sabatier [UPS] - Toulouse III</orgName>
<orgName type="institution">Institut National Polytechnique de Toulouse - INPT</orgName>
<orgName type="institution">Institut National des Sciences Appliquées (INSA) - Toulouse</orgName>
</affiliation>
</author>
<author><persName><forename>Mohamed Salah</forename><surname>Bouassida</surname></persName>
<affiliation>
<orgName type="laboratory">HEUDIASYC</orgName>
<orgName type="team">Heuristique et Diagnostic des Systèmes Complexes</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR6599</orgName>
<orgName type="institution">Université de Technologie de Compiègne</orgName>
</affiliation>
</author>
<author><persName><forename>Najah</forename><surname>Chridi</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA / LIFC</orgName>
<orgName type="team">CASSIS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : FRE2661</orgName>
<orgName type="institution">Université de Franche-Comté</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Isabelle</forename><surname>Chrisment</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">MADYNES</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Laurent</forename><surname>Vigneron</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA / LIFC</orgName>
<orgName type="team">CASSIS</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : FRE2661</orgName>
<orgName type="institution">Université de Franche-Comté</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<title type="main" level="a">UML Modeling and Formal Verification of Secure Group Communication Protocols</title></analytic><monogr><title level="m" type="main">Second IEEE International workshop UML and Formal Methods (UML&FM'2009)</title><meeting>Second IEEE International workshop UML and Formal Methods - UML&FM'2009</meeting><imprint><pubPlace><settlement>Rio de Janeiro</settlement><country>Brazil</country></pubPlace><biblScope type="publicationDate">2009-00-00</biblScope><biblScope type="pp">--</biblScope></imprint></monogr><idno type="HALid">http://hal.archives-ouvertes.fr/hal-00447668</idno></biblStruct>
</listBibl>
</listBibl>