[go: up one dir, main page]
Communication Dans Un Congrès Année : 2004
A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols
Yannick Chevalier (1) , Luca Compagna (2) , Jorge Cuellar (3) , Paul Hankes Drielsma (4) , Jacopo Mantovani (2) , Sebastian Moedersheim (4) , Laurent Vigneron (1)
1 CASSIS - Combination of approaches to the security of infinite states systems (France)
"> CASSIS - Combination of approaches to the security of infinite states systems
2 DIST - Department of informatics, systems and telecommunications (Italie)
"> DIST - Department of informatics, systems and telecommunications
3 Siemens AG [Munich] (Siemens AG (Headquarters) Wittelsbacherplatz 2 80333 Munich Germany - Allemagne)
"> Siemens AG [Munich]
4 D-INFK - Department of Computer Science [ETH Zürich] (Haldeneggsteig 4 / Weinbergstrasse 8092 Zürich - Suisse)
"> D-INFK - Department of Computer Science [ETH Zürich]

Résumé

This paper presents HLPSL, a high level protocol specification language for the modelling of security-sensitive cryptographic protocols. This language enjoys a formal semantics based on Lamport's Temporal Logic of Actions. HLPSL is modular and allows for the specification of control flow patterns, data-structures, alternative intruder models, and complex security properties. It is sufficiently high-level to be accessible to protocol engineers (themselves not necessarily formal methods experts), yet easily translatable into a lower-level term-rewriting based language well-suited to model-checking tools. The accommodation of these contrasting features makes HLPSL able to easily specify modern, industrial-scale protocols on which existing specification languages only partially succeed.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
A04-R-183.pdf (187) Télécharger le fichier

Publications Loria  : Connectez-vous pour contacter le contributeur

https://inria.hal.science/inria-00099882

Soumis le : mardi 26 septembre 2006-10:02:03

Dernière modification le : jeudi 27 février 2025-03:17:38

Archivage à long terme le : mercredi 29 mars 2017-12:51:37

Télécharger pour visualiser

Dates et versions

inria-00099882 , version 1 (26-09-2006)
Identifiants
  • HAL Id : inria-00099882 , version 1

Citer

Yannick Chevalier, Luca Compagna, Jorge Cuellar, Paul Hankes Drielsma, Jacopo Mantovani, et al.. A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols. Workshop on Specification and Automated Processing of Security Requirements - SAPS'2004, 2004, Linz, Austria, 13 p. ⟨inria-00099882⟩

Exporter

BibTeX XML-TEI Dublin Core DC Terms EndNote DataCite

Collections

CNRS INRIA UNIV-FCOMTE UNIV-BM FEMTO-ST UNIV-BM-THESE UNIV-LORRAINE INRIA2 LORIA LORIA-FM
767 Consultations
905 Téléchargements

Partager

More