After seeing Goldwasser and Bellare's lecture notes on provable
security recommended here, I decided to read them. I knew nothing
about this subject before and they seem very good. In particular I
enjoyed reading chapters 5 and 6. They examine ECB, CBC and CTR modes
of block ciphers. I was curious about how 'strong' other modes are
(in particular CFB mode) so I searched Google for "IND-CPA CFB" and
found very little.
What I did find though was a project at UC Berkeley in which one could
examine this particular mode and its resistance to chosen plaintext
attacks. But I find the project description strange. Here's the
description
"Give a correct proof of security for CFB mode encryption. Handle the
case of m-bit CFB mode, for small values of m, if you can. "
The first thing that bugs me is the word "correct". Surely a proof
is, by definition, "correct"? Are there a number of erroneous
"proofs" for CFB mode out there?
The second thing that interests me is the phrase "for small values of
m". Obviously if you've got a block cipher with block size n, then
you can model the cipher when used in n-bit CFB mode as a PRP.
However for m<n, the cipher cannot be modelled as a PRP and modelling
it as a PRF is dubious since it's a very well-behaved PRF. Is the
requirement "for small values of m" because the block cipher in m-bit
CFB mode looks more like a PRF for small values of m?
That was my fault. Sorry for the confusion. That was from a course
I taught: it was on a list of potential research projects that students
could do for their term project.
The background is that the following paper claimed, at FSE 2001, to
have a proof that m-bit CFB mode is IND-CPA secure for all m:
A. Alkassar, A. Geraldy, B. Pfitzmann, A.-R. Sadeghi,
"Optimized Self-Synchronizing Mode of Operation", FSE 2001.
http://www.sirrix-ag.de/research/res.publikationen/ressource/AGPS_01OCFB-paper.ps
However, upon reading it carefully, I discovered that their proof is
bogus. That inspired my suggestion to look for a correct proof.
I have since discovered a more recent paper that appears to give a
correct proof of IND-CPA security for n-bit CFB mode (n = block width):
P.A. Fouque, G. Martinet, G. Poupard,
"Practical Symmetric On-line Encryption", FSE 2003.
http://www.di.ens.fr/~fouque/fse03.pdf
Strangely, the authors of the FSE 2003 paper did not seem to be aware
of the prior FSE 2001 work; it was not cited in their paper. Anyway,
the FSE 2003 security proof only applies to n-bit CFB mode, and requires
that the IV be random. That's good, because if the IV is not random,
there are attacks. See here for slides illustrating some of the attacks:
David Wagner, "New attacks on t-bit OFB and CFB modes:
A cautionary note regarding IV selection", CRYPTO 2002 rump session.
http://www.cs.berkeley.edu/~daw/talks/ofb-crypto02.ps
Meanwhile, one of the students in my class independently worked out a
proof of a similar result, which I also believe to be correct. So,
I now have confidence in the security of CFB, when used properly.
As far as I know, the historical comments above have never appeared
in the published literature. Perhaps I ought to get around to writing
this up someday, if I ever get time, but it just hasn't seemed that
important to me.
By the way, I'm not aware of anyone who has analyzed the security of
m-bit CFB for m < n, so this remains an open question as far as I know.
>The second thing that interests me is the phrase "for small values of
>m". Obviously if you've got a block cipher with block size n, then
>you can model the cipher when used in n-bit CFB mode as a PRP.
>However for m<n, the cipher cannot be modelled as a PRP and modelling
>it as a PRF is dubious since it's a very well-behaved PRF. Is the
>requirement "for small values of m" because the block cipher in m-bit
>CFB mode looks more like a PRF for small values of m?
It's still an interesting question even if we model the m-bit
truncated block cipher as a PRF. In fact, this is a pretty reasonable
assumption.
First, there is a standard result, known as the PRP/PRF
switching lemma, that says the following: if E is a (t,q,e)-PRP
with a n-bit block, then it is also a (t,q,e + q^2/2^n)-PRF. Obviously,
truncation of a PRF cannot hurt, so the consequence also applies to
truncated versions of E. Note that if the number q of chosen-plaintext
queries that an attacker can make to E is quite small, then this shows
that the strength of E as a PRF is almost as good as its strength as
a PRP. However, once q gets near 2^{n/2} (the "birthday bound"), this
lemma tells you essentially nothing about the strength of E as a PRF.
If you don't truncate, then this lemma is tight: there are attacks of
roughly matching complexity. However, there has been some more recent
work showing that truncation actually improves security. The following
two papers show that if E is a (t,q,e)-PRP and we truncate it down to
m bits, then the result will be a (t-O(q),q,e')-PRF, where
e' = O(n sqrt(q) 2^{m-n}) if 0 < q <= 2^m
e' = O(n q 2^{m/2 - n}) if 2^m < q <= 2^{n - m/2}
The result above is from the following two papers:
M. Bellare and R. Impagliazzo, "A tool for obtaining tighter
security analyses of pseudorandom function based constructions,
with applications to PRP to PRF conversion", eprint 1999/024.
http://eprint.iacr.org/1999/024/
The problem was previously analyzed in the previous paper
C. Hall, D. Wagner, J. Kelsey, B. Schneier,
"Building PRFs from PRPs", CRYPTO '98.
http://www.cs.berkeley.edu/~daw/papers/prf-crypto98-long.ps
which showed a corresponding result with
e' = 5 q^{2/3} 2^{(m-2n)/3} + q^3 2^{-2k-1}
I'm not aware of any subsequent work on this topic; attention on the
topic of building PRFs out of PRPs has moved on to other constructions
with better properties than simple truncation.
Anyway I'll follow up the refs above.
I presume that trying to prove the switching lemma would be a good
exercise for me?
Goldwasser & Bellare is good. You might have to dive in to papers
after that.
>I presume that trying to prove the switching lemma would be a good
>exercise for me?
Yeah, that's a good exercise. It is instructive.
I've been reading through Bellare and Rogaway's notes and they're good
too. They have exercises, which is always a big help.
The flaw is in Lemma 1.
I can give you a more thorough explanation if you'd like.
Did you want a chance to work this out yourself, or did you
just want to see an explanation of the bug in the proof?
The one claim in Lemma 1 that I had noticed that seems bogus was this
"We do this for the case with random ... IV. (THE DIFFERENCE IN THE
OTHER CASE IS NEGLIGIBLE)." The difference isn't negligible. If the
IV isn't random but is all zeroes (or all ones) and the cipher is
being used in 1-bit CFB mode then an adversary who sends the challenge
message pairs (m0=0, m1=0) followed by (m0=0, m1=1) will be able to
determine which message an oracle is encrypting 75% of the time, i.e.
with advantage 0.5. In fact for m-bit CFB mode where m is small, the
adversary always has a large advantage.
My guess is that this is what I should be investigating: for small m,
try to get the contents of the feedback register to some previously
seen value and to show that their "birthday paradox"-like bound can't
be taken for granted (even for a random IV).
Not at all.
>The one claim in Lemma 1 that I had noticed that seems bogus was this
>"We do this for the case with random ... IV. (THE DIFFERENCE IN THE
>OTHER CASE IS NEGLIGIBLE)." The difference isn't negligible. If the
>IV isn't random but is all zeroes (or all ones) and the cipher is
>being used in 1-bit CFB mode then an adversary who sends the challenge
>message pairs (m0=0, m1=0) followed by (m0=0, m1=1) will be able to
>determine which message an oracle is encrypting 75% of the time, i.e.
>with advantage 0.5. In fact for m-bit CFB mode where m is small, the
>adversary always has a large advantage.
Ding ding ding. Yup, that's the flaw that I know about.
I think you're done. You've shown an attack. m-bit CFB mode is not
secure for small m, if IVs are chosen poorly. That contradicts the
statement of Lemma 1.
That doesn't mean that CFB is always insecure, or that their proof is
wrong in all cases. But it is certainly wrong in at least some cases,
and part of the reason is that it is too sketchy in some important places.
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.
Perhaps if I spent more time thinking carefully about their proof, I
could satisfy myself about how to fill in the gaps in the case where m
is large or where IVs are chosen randomly.
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.
I don't know of anyone using Mizar or HOL. On the other hand, there is
active research in trying to use "formal methods" to prove security of
cryptographic protocols, or at least find flaws in cryptographic protocols.
This is higher level than what you are asking for (e.g. current formal
methods will not help you prove a hybrid argument from scratch).
It may still be of interest.
Jonathan Herzog at MIT has some slides explaining the formal methods
approach
http://theory.lcs.mit.edu/~jherzog/talks/intro-to-red-crypto.pdf
(Formal methods is sometimes referred to as "red cryptography," while
the reduction-based approach is sometimes referred to as "blue
cryptography." This has nothing to do with US politics as far as I know.
I believe the terms originate from a survey paper published long before
the 2004 US elections.)
One of my favorite uses of formal methods was to find flaws in an
"abuse-free" contract signing protocol. The protocol came with a proof
of security which was correct as far as it went; model-checking revealed
shortcomings in the definition of security.
"Finite-State Analysis of Two Contract Signing Protocols"
John Mitchell and Vitaly Shmatikov
http://www.cs.utexas.edu/~shmat/abstracts.html#fair
Incidentally, you can download the Mur\phi tool used for that paper
http://verify.stanford.edu/dill/murphi.html
so you can in principle redo the analysis or extend to your own
favorite protocols.
Recently there has been an attempt to "marry" the formal methods
approach and the reduction-based approach. An overview and initial
step can be found at
"Reconciling Two Views of Cryptography: The Computational Soundness
of Formal Encryption"
Martin Abadi and Phillip Rogaway
http://citeseer.ist.psu.edu/abadi00reconciling.html
It's also worth mentioning that Backes, Pfitzmann, and Waidner at IBM Zurich
have spent a lot of effort recently on building a library of "composable"
cryptographic primitives. The idea here is that you prove that composing
idealized primitives in certain ways yields a secure protocol, then provide
actual instantiations of the primitives and prove they meet the ideal.
"Universally Composable Cryptographic Library"
http://citeseer.ist.psu.edu/backes03universally.html
That's just a scratch of the surface. There are actually many people working
in this area. For example, see this DIMACS workshop on security analysis
of protocols:
http://dimacs.rutgers.edu/Workshops/Protocols/abstracts.html
Again, this is all at the protocol level. As far as I know, these efforts
won't help you prove the "obvious" things. Along those lines, there was a
paper at FOCS 2003
which made some progress in formalizing the reasoning used in cryptographic
proofs in a way sufficient to obtain formal proofs of some basic theorems:
"Logics for reasoning about cryptographic constructions"
R. Impagliazzo and B. M. Kapron
http://citeseer.ist.psu.edu/624297.html
For example, they prove that given a PRG which stretches by 1 bit, you
can obtain a PRG which stretches by n bits via repeated application.
Unfortunately, at this point it seems to be a logic alone, without
tool support behind it. There may be other work or follow on
work.
In any case, I'd like to stress I'm not an expert in this area -- I just
keep my ears open. There's likely an ocean of stuff I don't know about.
Still, there are a few things you may find worth looking at for your own
interests.
-David Molnar