HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 Connect in order to contact the contributor
Submitted on : Wednesday, October 11, 2006 - 4:14:17 PM
Last modification on : Friday, February 4, 2022 - 3:23:31 AM
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

356

Files downloads

39