Subject: Re: [RPSEC] proposed message to the IESG

From: Sandy Murphy <[email-masked]>
Date: Thu, 20 Jan 2005 16:50:17 -0500 (EST)

>Russ White.... believes the specifications requirement should be based on 
>an analysis of what is provable

Russ, I've really tried to hold back responding to your frequent
mentions of "proof", "provable", "impossible to prove", etc.

Now, to me and some people like me, this leads to the following sorts
of considerations:  "Well, first we'll have to agree on a logical
system and I sure hope we can avoid natural logic because I've found
the law of excluded middle too helpful to give it up and then we'll
have to agree on some axioms and particularly a rule of inference
and I don't see that we'll need anything more than good old
modus ponens ...."

Which is all a grandiose and hopefully diverting way to say that
proofs are something you construct in a formal way in a formal
system that you've jointly agreed to.

I think you mean "convincing" when you say "proof" and you and
Steve aren't agreeing to the same ground rules to convince each
other.

To some people, proofs of security features go something like this:
(a) the spec says things should happen like this
(b) it is possible to make things not happen like this
(c) QED

OK, so I'm generalizing a lot.  But the core point is that security
relies on assumptions holding.  Sometimes those are innate (the IP
address in the source field is the address of where this comes from)
and sometimes it derives from the spec (the spec says that the message
I received is generated when the source received my message, therefore
I can assume that the source received my message).

--Sandy

_______________________________________________
RPSEC mailing list
[email-masked]
https://www1.ietf.org/mailman/listinfo/rpsec

---

From: Russ White <[email-masked]>
Date: Thu, 20 Jan 2005 18:27:20 -0500 (Eastern Standard Time)

> I think you mean "convincing" when you say "proof" and you and Steve 
> aren't agreeing to the same ground rules to convince each other.
>

> (b) it is possible to make things not happen like this

The problem is in this: How do you describe what the specification 
specifies?

-- Is there a concept of an "end to end" thing called an "update," and 
you're trying to prove "authorization" to readvertise this "update?"

-- Are you trying to prove certain things about the information advertised 
to you by a peer (using an update, with many other pieces of information in 
it), are "true," in some sense? What are the questions we need to ask about 
this information?

IMHO, just because the BGP specification says "the update is then processed 
using method x...." doesn't mean an "update" exists as an atomic thing 
within BGP.

> address in the source field is the address of where this comes from) and 
> sometimes it derives from the spec (the spec says that the message I 
> received is generated when the source received my message, therefore I 
> can assume that the source received my message).

Yes, exactly. IMHO, we should ask what we can prove about a specific piece 
of information, and require certain things be found true. For instance, 
saying: "I want to prove this update was received from x, at time y, and 
hasn't been altered," doesn't answer any real questions. _Why_ do you want 
to prove those things? What is it you hope to prove by showing this update 
came from x at time y?

If the answer is anything other than: "proving the packet was transported 
along a certain path at a certain time," then you're not at the 
requirements stage--you're still at the solutions stage, simply trying to 
push a solution off as a requirement.

When the data is opaque, and the packet is "pushed into a tunnel" on one 
end, and "pulled out of the tunnel" at the other end, you have end-to-end 
security. If you're looking for end-to-end security, it might be sufficient 
to prove every node along the way touched the packet in a certain way.

It's a completely different game when everyone along the way can pull the 
information out, repackage it, and possibly alter it. There's no concept of 
"end-to-end" in the BGP protocol in this way.

Let me also point out that I assert an "update" isn't what I'm interested 
at all in BGP. I'm interested in a prefix and it's attributes. One of those 
attributes happens to be the as path, and you can make assertions about 
that as path. There's no such thing as "the update" in the same sort of 
context as "the packet" in an IP flow.

:-)

Russ

__________________________________
[email-masked] CCIE <>< Grace Alone