An Isabelle formalization of protocol-independent secrecy with an application to e-commerce

Frédéric Blanqui 1, 2
2 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : A protocol-independent secrecy theorem is established and applied to several non-trivial protocols. In particular, it is applied to protocols proposed for protecting the computation results of free-roaming mobile agents doing comparison shopping. All the results presented here have been formally proved in Isabelle by building on Larry Paulson's inductive approach. This therefore provides a library of general theorems that can be applied to other protocols.
Type de document :
Autre publication
2002
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00105606
Contributeur : Frédéric Blanqui <>
Soumis le : mercredi 11 octobre 2006 - 16:14:17
Dernière modification le : jeudi 10 mai 2018 - 01:33:43
Document(s) archivé(s) le : mardi 6 avril 2010 - 19:24:14

Fichiers

Identifiants

Collections

Citation

Frédéric Blanqui. An Isabelle formalization of protocol-independent secrecy with an application to e-commerce. 2002. 〈inria-00105606〉

Partager

Métriques

Consultations de la notice

270

Téléchargements de fichiers

103