Fragmentation protocols

frag.rst

Fragmentation protocol

Parties

the transport

• the party that controls the physical communication. for example yourrouter, or your IRCS network (the set of servers)
• note that in an IRC network where one or more links are non-SSL then the whole world is effectively the IRC network

"entity"

some user of the transport. note that in an unsecure transport such as IP or IRC, the whole world is effectively every entity

"packet"

each packet claims a from: field. this claim may not actually be true. (the source of the claim is irrelevant for our analysis, it could be the transport or some attacker.)

"fragment"

a packet that cannot be processed by higher layers because it needs to be joined with some other fragments.

"full-packet"

the reconstructed form of several fragments

"fragmentation protocol"

an algorithm that reconstructs fragments into full-packets, by buffering fragments in memory until its full-packet is reconstructed. a protocol may also drop a buffered fragment actually-from E when:

1. after a timeout
2. on receipt of another fragment actually-from E
3. on receipt of another fragment actually-from F != E

Security properties

1. DoS of local system resources
2. DoS of full-packets
   • an attacker cannot purposefully prevent {a full-packet actually-from:A} from being reconstructed by an intended recipient
3. DoS of fragments
   • an attacker cannot purposefully cause a fragment actually-from E to be rejected by an intended recipient, even if it was buffered for a while.
   • for example, fragment#1 claimed-from E but not actually-from E is accepted and concatenated onto fragment#1 that was actually-from E, causing it to fail end-to-end verification later

Propositions / threat assumptions

Not all of these are used in all theorems.

1. For a given sender E, every fragment is part of a full-packet and they send these in the correct order. (i.e. E is "honest" in the context of P)
2. There is no attacker who can drop or alter packets.
3. There is no attacker who can forge the from: field on any packet. In other words, the protocol P is able to ignore packets whose claimed-from is not actually-from.
4. For every entity E, the protocol does not reject packets actually-from E because of packets from other entities F != E (i.e. reason (c) in our list of reasons).
5. An attacker is unable to create >n distinct entities on the transport, where n*m is the limit of the local system resources, and m is the amount of resources-per-entity the protocol is willing to allocate.
6. For a given protocol P, P performs end-to-end verification of every from: field.
7. For a given transport S, S performs transport verification of every from: field.

• e.g. an IRCS network could enforce that the nickname Bob can only send packets via a specific SSL connection (from IP $addr to IRC server $addr).

Security definition

A fragmentation protocol P is "secure" if it:

• P achieves #1 in all situations.
• If #B is true, and for all entities E where #A is true, P achieves #2 and #3. (We must assume #B here because of Lemma #1).

Lemmas

Lemma 0

There exists some protocol P that achieves #1 in all situations, regardless of external parties.

Proof: Use of local system resources may be controlled independently of any external party or protocol specification - e.g. via local resource tracking measures, such as size and time constraints. []

Lemma 1

If #B is false, then #2 is impossible (¬exists some P that achieves #2).

Proof: The attacker can always drop or alter fragment#1 of a full-packet. []

Lemma 2

If #F is true or if #G is true, then #C is true.

Proof: by definition of #F, #G respectively. []

Lemma 3

If #A and #B are true, then Property #2 and #3 are equivalent.

Proof:

• #2 implies #3: If every full-packet is reconstructed, then none of its fragments were rejected. We assume #A, so this covers all fragments, so we have #3.
• #3 implies #2: If every fragment is not rejected, and we assume #B, then every fragment will be received (and never rejected). Furthermore if we assume #A then every one of these is part of a full-packet, which will eventually be reconstructed, so we have #2.

[]

Theorem 1

If #A, #B, #C, #D are all true, then P achieves #3.

Proof:

When receiving a fragment f claimed-from E, this is actually-from E (by #C).

The protocol might reject f later because:

1. of a timeout
   • but this is ruled out because we assume #A and #B
2. due to receiving other fragments actually-from F != E (by #C)
   • but this is ruled out because we assume #D
3. due to receiving other fragments actually-from E
   • but this is ruled out because we assume #A

Therefore f is never rejected, independently of P (as long as it is a fragmentation protocol, i.e. it follows the "valid rejection reasons). []

Theorem 2

If #D, #E are true, then P achieves #1.

Proof:

TODO

Theorem 3

If #D, #C is true, then P is "secure".

Proof:

Something about Theorem 1 and Theorem 2.

TODO

Theorem 4

A {protocol P where #F is true} does not have more security properties than a {protocol Q where #F is false}, except for when #B is true and #C is false.

(Assume #D is true for both P and Q.)

Proof:

Protocol P: #F implies #C (Lemma 2), so P satisfies #C, so (by Theorem 3) P is "secure".

Protocol Q:

1. If #G is true, then this also implies #C, so Q is also secure. (same as above reasoning)
2. If #G is false, then either #C is true in which case Q is secure, or #C is false in which case Q may be not secure. []