RE: SOI QUESTIONS: 2.6 Formal proofs of security

[Ran Canetti <canetti@watson.ibm.com>]

Phill, 

I'm glad we're in agreement. The reason that I went into this long exposition
of security analysis methods is that I got the feeling from the discussion
that some people may be mistakenly equating "rigorous analysis of protocols" 
with "formal methods".

A good set of empirical tests is always welcome. But I fear that any set of 
specific empirical tests would be unable to provide the desired level of 
confidence. (what if there is another attack that we didnt think of.)

I personally favor cryptographic analysis. Here you can rigorously
claim that the protocol cannot be broken - by *any* attacker - unless you
actually break the underlying computational assumption. (This is done by 
showing how to turn *any* attacker that breaks the protocol into an algorithm 
that solves the underlying intractable problem.)

Ran


BTW, in this vein, there is a paper by Hugo and me in the upcoming crypto
conference that rigorously proves the security of the cryptographic protocol
that stands at the core of both IKEv1 (sig modes), IKEv2 (sig mode), and JFKr. 
This is not intended as full analysis of either of those protocols, but it 
demonstrates that the core of those protocols is secure.





> From pbaker@verisign.com Wed Jun 26 11:15:41 2002
> 
> In response to Ran's note I suspect that all the people in the thread
> actually have a mutually compatible view of what formal methods can do and
> what should be required.
> 
> Some of the negativity in my posts probably comes from the fact that having
> seen Formal methods massively oversold I think it is important to set
> expectations.
> 
> Clearly formal methods can add significant value. However what people have
> been cautioning against is setting the bar to SOI to be a formal 'proof of
> security' ignoring the fact that what consitutes a proof of security is
> highly debatable (even in forums other than IETF mailing lists where
> anything is highly debatable), and the fact that we did not put IKE through
> that analysis.
> 
> I think it would be quite reasonable to state specific empirical tests that
> a SOI protocol should pass, provided that the analysis methods involved do
> not introduce arbitrary constraints into the solution space whose only
> purpose is to allow the analysis.
> 
> 		Phill
> 

ipsec@lists.tislabs.com Thu Jun 27 14:30:19 2002
Received: from sp1n293en1.watson.ibm.com (sp1n293en1.watson.ibm.com [9.2.112.57])
	by ornavella.watson.ibm.com (AIX4.3/8.9.3/8.9.3/01-10-2000) with ESMTP id OAA33530
	for <canetti@ornavella.watson.ibm.com>; Thu, 27 Jun 2002 14:30:18 -0400
Received: from igw2.watson.ibm.com (igw2.watson.ibm.com [9.2.250.12])
	by sp1n293en1.watson.ibm.com (8.11.4/8.11.4) with ESMTP id g5RIUIL29468;
	Thu, 27 Jun 2002 14:30:18 -0400
Received: from lists.tislabs.com (portal.gw.tislabs.com [192.94.214.101])
	by igw2.watson.ibm.com (8.11.4/8.11.4) with ESMTP id g5RIUC228526;
	Thu, 27 Jun 2002 14:30:12 -0400
Received: by lists.tislabs.com (8.9.1/8.9.1) id NAA23303
	Thu, 27 Jun 2002 13:57:09 -0400 (EDT)
From: "Theodore Ts'o" <tytso@mit.edu>
To: ipsec@lists.tislabs.com
Subject: SOI QUESTION: 4.5 SA rekeying
Phone: (781) 391-3464
Message-Id: <E17NdiF-0000fL-00@think.thunk.org>
Date: Thu, 27 Jun 2002 14:09:47 -0400
Sender: owner-ipsec@lists.tislabs.com
Precedence: bulk


Please discuss and answer this question:

4.5 SA rekeying

4.5.A) Both JFK and IKEv2 provide SA rekeying.  The functionality
provided is roughly identical, although JFK requires more
cryptographic operations to do rekeying (see 2.4).  Does anyone care
about how low-level implementation details of IKEv2 and JFK?

Implications from the Scenarios:

[none]