面向电子商务的协议独立保密性的 Isabelle 形式化
计算机科学中的逻辑
2016-08-16 v1
摘要
建立了一个协议独立的保密性定理，并应用于几个非平凡协议。特别是应用于保护自由漫游移动代理进行比较购物计算结果的协议。此处呈现的所有结果都在 Isabelle 中通过建立在 Larry Paulson 归纳方法之上的形式化证明。由此提供了一个可应用于其他协议的通用定理库。
引用
@article{arxiv.cs/0610069,
title = {An Isabelle formalization of protocol-independent secrecy with an application to e-commerce},
author = {Frédéric Blanqui},
journal= {arXiv preprint arXiv:cs/0610069},
year = {2016}
}