An Isabelle formalization of protocol-independent secrecy with an application to e-commerce
<|reference_start|>An Isabelle formalization of protocol-independent secrecy with an application to e-commerce: 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.<|reference_end|>
@article{blanqui2006an,
    title={An Isabelle formalization of protocol-independent secrecy with an
  application to e-commerce},
    author={Fr'ed'eric Blanqui (INRIA Futurs)},
    journal={arXiv preprint arXiv:cs/0610069},
    year={2006},
    archivePrefix={arXiv},
    eprint={cs/0610069},
    primaryClass={cs.LO}
}