Skip to Main content Skip to Navigation
Other publications

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.
Document type :
Other publications
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/inria-00105606
Contributor : Frédéric Blanqui <>
Submitted on : Wednesday, October 11, 2006 - 4:14:17 PM
Last modification on : Wednesday, September 16, 2020 - 4:51:26 PM
Long-term archiving on: : Tuesday, April 6, 2010 - 7:24:14 PM

Files

Identifiers

Collections

Citation

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

Share

Metrics

Record views

480

Files downloads

134