Re: IND-CPA for CFB mode
From: Paul Rubin (//phr.cx_at_NOSPAM.invalid)
Date: 08 Oct 2004 01:17:09 -0700
email@example.com (David Wagner) writes:
> Personally, I don't like "proofs" with gaps. I'm too lazy to work
> hard on trying to figure out whether such gaps can be filled. And,
> I don't trust proofs where authors don't spell out all the details (it
> makes me wonder whether the authors themselves have done the exercise
> of working out the details carefully). That's my thinking, anyway.
All security proofs I've seen have gaps of a type that experts have
gotten used to and understand. They also sometimes have painfully
detailed proofs of things that are obvious. The result is when I try
to prove something myself as a non-expert, I don't know if I've proved
it or not. And obvious statements often resist my attempts at writing
out simple proofs.
I've been wondering for a while whether anyone has tried writing out
any security proofs formally, i.e. in a system like Mizar
(www.mizar.org) or HOL (http://www.cl.cam.ac.uk/Research/HVG/HOL/).
This is going to have to be done eventually.