Language Design for Computationally Sound Communications Abstractions

Abstract : We are interested in computationally sound implementations for languages of distributed communicating processes, with secure high-level primitives for authentication and secrecy, but without explicit cryptography. We develop such an implementation for a variant of the pi calculus [6]. In this language, security properties can be studied using traces and equivalences that account for the presence of an arbitrary (abstract) adversary that controls the network. The cryptographic implementation of the language uses standard primitives and assumptions; it guarantees that these abstract properties also hold in a concrete, distributed setting, against probabilistic polynomial-time active adversaries. At FCC'06, we intend to review and discuss the design space for programming languages with cryptographically sound implementations. In particular, we motivate some unusual design choices for our language, we discuss its current limitations, and we consider possible extensions.
Type de document :
Communication dans un congrès
Véronique Cortier et Steve Kremer. Workshop on Formal and Computational Cryptography (FCC 2006), Jul 2006, Venice/Italy, 2006
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00080672
Contributeur : Véronique Cortier <>
Soumis le : mardi 20 juin 2006 - 15:03:51
Dernière modification le : mardi 20 juin 2006 - 15:27:50
Document(s) archivé(s) le : lundi 5 avril 2010 - 23:06:21

Fichier

Identifiants

  • HAL Id : inria-00080672, version 1

Collections

Citation

Pedro Adao, Cédric Fournet. Language Design for Computationally Sound Communications Abstractions. Véronique Cortier et Steve Kremer. Workshop on Formal and Computational Cryptography (FCC 2006), Jul 2006, Venice/Italy, 2006. 〈inria-00080672〉

Partager

Métriques

Consultations de la notice

108

Téléchargements de fichiers

36