3 ms·

There are a number of components there. (1) Protocols are very sensitive to errors, possibly more than primitives. If you screw up the internals of a primitiv

There are a number of components there. (1) Protocols are very sensitive to errors, possibly more than primitives. If you screw up the internals of a primitive, the results will be different (and visibly so), but it stands a good chance at still being secure. Protocols however tend to be very tightly designed. Modifications that have a working happy path are more likely to have significant wholes: a missing check, failure to authenticate part of the transcript, loss of forward secrecy… No real justification there, it just has been my experience dealing with modern primitives and protocols. (2) Correctness subsumes security. A program is correct if it fulfils its requirements. A program is secure if it fulfils its security requirements. Which by definition are a subset of all requirements. That said, while immunity to relevant side channels are definitely parts of security requirements, it helps to separate them from the correctness of end results. (3) Bug free code is possible. It's not easy, but it can be done. Constant time implementations of modern primitives are among the easiest code to test, ever: since code paths only depend on the lengths of parameters, testing them all against a reference is trivial. That's not just "100% code coverage", it's 100% path coverage. As for the proofs, while they may not be easy to produce, the good ones are fairly easy to follow (though extremely tedious), and the great ones can be checked by a machine, making them trivial to verify.

tialaramex 6y ago
> As for the proofs, while they may not be easy to produce, the good ones are fairly easy to follow (though extremely tedious), and the great ones can be checked by a machine, making them trivial to verify. The main value from protocol level proofs is that since you need to tell the machine your assumptions before it spits out a proof, a careful proof development process can discover unstated assumptions. The TLS Selfie attack is an example. In principle this attack could have been found during proof generation for TLS 1.3, but in practice the proofs generated during TLS 1.3 development smuggle in an unstated assumption that means Tamarin rules out Selfie even though in some cases it would be a viable attack. [Selfie goes like this: Alice and Bob have a PSK for authentication, Mallory doesn't know the PSK, but Mallory can interfere with the network between Alice and Bob. Alice intends to ask Bob, "Do you have the car?". Mallory can't read this question or write an answer Alice will accept because they don't know the PSK. However, Mallory just redirects the question back to Alice. "Do you have the car?" and Alice doesn't have the car, so she answers "No" and she knows the PSK so her answer is proper. Now Alice gets an answer to her question, "No" and so she concludes Bob doesn't have the car. But actually Bob was never asked!] Knowing about this, it can be repaired. Alice and Bob simply address the intended recipient in each message, "Bob, do you have the car?" "No Alice, I don't" - and check for their own name in messages they receive. Or they use a separate PSK for each direction, not just one per pair of participants in their system. Or they can choose only to either be a TLS client or a server and never both. But all these steps aren't obvious if there's nowhere stated the assumption that you did one of these three things. Intuitively it seems as though since Mallory doesn't know the PSK and the Tamarin prover says this protocol works you're fine.
- jorangreef 6y ago
  Thanks for the excellent example of the TLS Selfie attack. Having worked on protocols, I have found again and again that making the context explicit by cryptographically binding intent to the message is paramount.
zrm 6y ago
> Protocols are very sensitive to errors, possibly more than primitives. If you screw up the internals of a primitive, the results will be different (and visibly so), but it stands a good chance at still being secure. I don't know if I agree with this. You can easily write an implementation of a primitive that even creates the correct output bytes while leaking secrets via every side channel, or via the one side channel you didn't realize existed. I also think that "protocol" is too wide to be a useful category. TLS is a protocol, right? But what about HTTPS? Your site's API? There is always going to be cryptography at the bottom, but at some point you have to draw a line or "don't roll your own crypto" becomes "don't write your own software" because everything is in scope. Or maybe you can't draw that line because the upper layer stuff still has implications. Think about the compression oracle attacks. The upper layer has secret data, compresses it and then shovels it through a "secure" protocol but has already leaked the secret contents through the content size difference due to the compression. But if that means everything is in scope, what then?
- loup-vaillant 6y ago
  > or via the one side channel you didn't realize existed. Can't do much about that one. Gotta have someone telling you, or (worst case) the very state of the art advancing under your feet. > at some point you have to draw a line or "don't roll your own crypto" becomes "don't write your own software" because everything is in scope. Yes, there is a point beyond which you don't have a choice. The natural (and utterly impractical) line to draw is untrusted input. Talking through the internet is the obvious one, but merely playing a video exposes you to untrusted data that might take over your program and wreck havoc. Compression is a tough one. I'd personally try padding. Something like PADME should work well in many cases. https://en.wikipedia.org/wiki/PURB_(cryptography) https://en.wikipedia.org/wiki/PURB_(cryptography)
  - zrm 6y ago
    > Can't do much about that one. Gotta have someone telling you, or (worst case) the very state of the art advancing under your feet. But that's kind of the point. Primitives aren't easy either. Even one thought to be secure yesterday might not be today, which makes it easy to get wrong merely by relying on literature from a year ago rather than today. > The natural (and utterly impractical) line to draw is untrusted input. I think you're right about that, both as to where the line really is and as to how impractical that is if you don't want to just end up with essentially everything being in scope. > Compression is a tough one. I'd personally try padding. I'm not sure you can fix it strictly in the lower layers. The general attack works like this: The attacker can supply some data, the victim compresses that data and some secret data together and then sends the combination encrypted over a channel where the attacker can observe the size. If the attacker-supplied data matches the secret data, it can be compressed more so it gets smaller. The attacker's job is really easy if supplying one more byte of data that doesn't match the secrets causes the observed length to increase by one byte, but fixed padding just requires the attacker to find the padding boundary by supplying increasing amounts of pseudorandom (i.e. incompressible) data until the threshold for the next output size is reached, then swap in different bytes until some of them match the secret and it falls below that due to the compression. And random padding just requires more samples to account statistically for the randomness. In theory you might be able to fix it by making all messages the same length, but then if you want to support large messages, all messages become large, which could be unreasonably inefficient. And the whole point of the compression was to do the opposite of this. The real solution is not compressing attacker-supplied data together with secret data to begin with, but that means the upper layer has to know not to do that.

tialaramex 6y ago

> As for the proofs, while they may not be easy to produce, the good ones are fairly easy to follow (though extremely tedious), and the great ones can be checked by a machine, making them trivial to verify. The main value from protocol level proofs is that since you need to tell the machine your assumptions before it spits out a proof, a careful proof development process can discover unstated assumptions. The TLS Selfie attack is an example. In principle this attack could have been found during proof generation for TLS 1.3, but in practice the proofs generated during TLS 1.3 development smuggle in an unstated assumption that means Tamarin rules out Selfie even though in some cases it would be a viable attack. [Selfie goes like this: Alice and Bob have a PSK for authentication, Mallory doesn't know the PSK, but Mallory can interfere with the network between Alice and Bob. Alice intends to ask Bob, "Do you have the car?". Mallory can't read this question or write an answer Alice will accept because they don't know the PSK. However, Mallory just redirects the question back to Alice. "Do you have the car?" and Alice doesn't have the car, so she answers "No" and she knows the PSK so her answer is proper. Now Alice gets an answer to her question, "No" and so she concludes Bob doesn't have the car. But actually Bob was never asked!] Knowing about this, it can be repaired. Alice and Bob simply address the intended recipient in each message, "Bob, do you have the car?" "No Alice, I don't" - and check for their own name in messages they receive. Or they use a separate PSK for each direction, not just one per pair of participants in their system. Or they can choose only to either be a TLS client or a server and never both. But all these steps aren't obvious if there's nowhere stated the assumption that you did one of these three things. Intuitively it seems as though since Mallory doesn't know the PSK and the Tamarin prover says this protocol works you're fine.

jorangreef 6y ago
Thanks for the excellent example of the TLS Selfie attack. Having worked on protocols, I have found again and again that making the context explicit by cryptographically binding intent to the message is paramount.

zrm 6y ago

> Protocols are very sensitive to errors, possibly more than primitives. If you screw up the internals of a primitive, the results will be different (and visibly so), but it stands a good chance at still being secure. I don't know if I agree with this. You can easily write an implementation of a primitive that even creates the correct output bytes while leaking secrets via every side channel, or via the one side channel you didn't realize existed. I also think that "protocol" is too wide to be a useful category. TLS is a protocol, right? But what about HTTPS? Your site's API? There is always going to be cryptography at the bottom, but at some point you have to draw a line or "don't roll your own crypto" becomes "don't write your own software" because everything is in scope. Or maybe you can't draw that line because the upper layer stuff still has implications. Think about the compression oracle attacks. The upper layer has secret data, compresses it and then shovels it through a "secure" protocol but has already leaked the secret contents through the content size difference due to the compression. But if that means everything is in scope, what then?

loup-vaillant 6y ago
> or via the one side channel you didn't realize existed. Can't do much about that one. Gotta have someone telling you, or (worst case) the very state of the art advancing under your feet. > at some point you have to draw a line or "don't roll your own crypto" becomes "don't write your own software" because everything is in scope. Yes, there is a point beyond which you don't have a choice. The natural (and utterly impractical) line to draw is untrusted input. Talking through the internet is the obvious one, but merely playing a video exposes you to untrusted data that might take over your program and wreck havoc. Compression is a tough one. I'd personally try padding. Something like PADME should work well in many cases. https://en.wikipedia.org/wiki/PURB_(cryptography) https://en.wikipedia.org/wiki/PURB_(cryptography)
- zrm 6y ago
  > Can't do much about that one. Gotta have someone telling you, or (worst case) the very state of the art advancing under your feet. But that's kind of the point. Primitives aren't easy either. Even one thought to be secure yesterday might not be today, which makes it easy to get wrong merely by relying on literature from a year ago rather than today. > The natural (and utterly impractical) line to draw is untrusted input. I think you're right about that, both as to where the line really is and as to how impractical that is if you don't want to just end up with essentially everything being in scope. > Compression is a tough one. I'd personally try padding. I'm not sure you can fix it strictly in the lower layers. The general attack works like this: The attacker can supply some data, the victim compresses that data and some secret data together and then sends the combination encrypted over a channel where the attacker can observe the size. If the attacker-supplied data matches the secret data, it can be compressed more so it gets smaller. The attacker's job is really easy if supplying one more byte of data that doesn't match the secrets causes the observed length to increase by one byte, but fixed padding just requires the attacker to find the padding boundary by supplying increasing amounts of pseudorandom (i.e. incompressible) data until the threshold for the next output size is reached, then swap in different bytes until some of them match the secret and it falls below that due to the compression. And random padding just requires more samples to account statistically for the randomness. In theory you might be able to fix it by making all messages the same length, but then if you want to support large messages, all messages become large, which could be unreasonably inefficient. And the whole point of the compression was to do the opposite of this. The real solution is not compressing attacker-supplied data together with secret data to begin with, but that means the upper layer has to know not to do that.