inria-00179550, version 2

Automatic Methods for Analyzing Non-Repudiation Protocols with an Active Intruder

Francis Klay ¹, Judson Santiago ², Laurent Vigneron () ^a, 3

N° RR-6324 (2007)

• a –  UNIVERSITE NANCY 2
• 1:  France Télécom Recherche & Développement (FT R&D)
• http://www.francetelecom.com/fr/groupe/rd/
  France Télécom France
• 2:  DIMAp - UFRN, Natal (DIMAP - UFRN)
• 
  Universidade Federal do Rio Grande do Norte Brazil
• 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) France

Bibliographic reference

• Type of document: Research reports
• Domain:

  Computer Science/Cryptography and Security

  Computer Science/Logic in Computer Science

• Title: Automatic Methods for Analyzing Non-Repudiation Protocols with an Active Intruder
• Abstract: Non-repudiation protocols have an important role in many areas where secured transactions with proofs of participation are necessary. Formal methods are clever and without error, therefore using them for verifying such protocols is crucial. In this purpose, we show how to partially represent non-repudiation as a combination of authentications on the Fair Zhou-Gollmann protocol. After discussing its limits, we define a new method based on the handling of the knowledge of protocol participants. This method is very general and is of natural use, as it consists in adding simple annotations, like for authentication problems. The method is very easy to implement in tools able to handle participants knowledge. We have implemented it in the AVISPA Tool and analyzed the optimistic Cederquist-Corin- Dashti protocol, discovering two unknown attacks. This extension of the AVISPA Tool for handling non-repudiation opens a highway to the specification of many other properties, without any more change in the tool itself.
• Full text language: English
• Report type: Research Report
• Page number: 22
• Publication date: 2007
• Keywords: cryptographic protocols – non-repudiation – fairness – authentication – automatic analysis – AVISPA Tool
• Internal note: RR-6324

Attached file list to this document: 

TEX

paperKSV

rap-rech1.ps(19.5 KB)

RR-6324.tex(54.2 KB)

RRA4.sty(17.6 KB)

RR.sty(17.6 KB)

Logo-INRIA-couleur.ps(35.1 KB)

Logo-INRIA-Lorraine-couleur.ps(25.8 KB)

Logo-INRIA-picto.ps(24.4 KB)

PS

RR-6324.ps(318.4 KB)

PDF

RR-6324.pdf(269.8 KB)

• inria-00179550, version 2
• http://hal.inria.fr/inria-00179550
• oai:hal.inria.fr:inria-00179550
• From: Rapport De Recherche Inria <>
• Submitted on: Monday, 22 October 2007 08:39:29
• Updated on: Monday, 22 October 2007 08:40:26