@inproceedings{'CM6',
title = {Defending the bank with a proof assistant },
author = {Courant, Judica\"el and Monin, Jean-Fran\c{c}ois},
month = {MAR},
year = {2006},
booktitle = {{WITS 2006}},
address = {Vienna},
note = {In {WITS} proceedings},
team = {PACSS},
ps = {Docs/http://www-verimag.imag.fr/~monin/Publis/wits06.ps},
pdf = {Docs/http://www-verimag.imag.fr/~monin/Publis/wits06.pdf},
abstract = {We show how the proof-assistant Coq helped us formally verify the security of an API. As far as we know, this is the first mathematical proof of security of an API. The API we verified is a fixed version of Bond's modelization of IBM's Common Cryptographic Architecture. We explain the methodology we followed, sketch our proof and explain the points the formal verification raised.},
}
