Re: SOI QUESTIONS: 2.6 Formal proofs of security

[Eric Rescorla <ekr@rtfm.com>]

"Theodore Ts'o" <tytso@mit.edu> writes:

> Please discuss and answer this question.....  
> 
> 2.6 Formal proofs of security
> 
> 2.6.)  Does SOI need to provide a formal proof of security?  (Is this
> a "must have" or a "nice to have"?  What are we willing to trade-off
> for having a formal proof of security?)
I haven't decided how to answer this question, but I'd like to
amplify one of its possibly unnoticed consequences:

In many cases, the cryptographic primitives used by security protocols
do not have formal proofs of security either. In particular, 
IKEv2 [0] includes PKCS-1 by reference for digital signature. There
are no good formal proofs of security for PKCS-1 signature mode. Does
this mean we should cut over to one of the provably secure signature
schemes such as PSS? [1] I suspect that similar comments apply
the the key expansion prfs used by IKEv2.

It seems to me that if we're going to argue that protocols need
proofs of security that it probably follows that the primitives
need proofs of security to the extent possible. 

-Ekr

[0] JFK doesn't specify how signatures are performed but it
seems like a likely guess that they're PKCS-1.
[1] It's true we don't have a formal proof of security for
RSA but PKCS-1 isn't even known to be as strong as RSA.

-- 
[Eric Rescorla                                   ekr@rtfm.com]
                http://www.rtfm.com/