Axioms
Axioms
Posted Feb 21, 2021 6:22 UTC (Sun) by tialaramex (subscriber, #21167)In reply to: An introduction to lockless algorithms by gus3
Parent article: An introduction to lockless algorithms
Not explicitly stating such an assumption can get you in serious trouble if we want to prove things about a system.
For example: As an IoT developer thinking about how two devices you manufacture can securely communicate over an IP network, you might seize upon the Pre-shared Keys (PSKs) in TLS 1.3 (RFC 8446) as a good approach that avoids worrying about certificates or a PKI. It might seem like a common sense assumption that if device #1 ("Alice"), and device #2 ("Bob") share the same key K, that's going to be secure against any attacker that doesn't know K, the document (as published) doesn't suggest there would be any unexpected problems. And indeed mathematical proofs of TLS 1.3 say it does deliver on the claims in its introduction.
Unfortunately those proofs assume something different from you. They assume your two devices would each need their own key, K1 and K2. If you don't use separate keys you need countermeasures not described in the protocol, because of the "Selfie attack". The attack goes like this, Alice asks Bob something (using key K of course), but Mallory (who doesn't know K) just redirects Alice's message back to Alice. Alice thinks this question came from Bob (after all it uses key K which they share) and answers it, now Alice also thinks that answer came from Bob. Mallory has successfully confused Alice despite being unable to either read or forge messages from either Alice or Bob. Under the proof scenario Alice asks using K1, when the message is redirected back to her Alice is puzzled because it isn't encrypted with key K2 from Bob, so that message is rejected and everything is fine.
If this assumption had been made into an explicit _axiom_ that could have highlighted that the TLS document doesn't explain the problem with just having a single key K and likely its authors would have drafted a section explaining why you might need more keys than seem necessary at first glance, and what alternative strategies would work if you must have one key.
A more broadly famous missing assumption is the Axiom of Choice. In the 1800s mathematicians were confident they understood the Theory of Sets - they had established Axioms stating how it works - but alas they'd actually without making it explicit been assuming that in a set of sets (like the set of sets of integers) you can always choose one of the members of each set. This is definitely true for finite sets. But for infinite sets we can't prove it, so, we ought to explicitly make it an Axiom and say so, if we're wrong any results depending on that assumption may be wrong too. Today most mathematicians will choose ZFC, axioms for set theory which include the Axiom of Choice, because it does after all _feel_ intuitively as though you could choose one from each set. But at least you've written down this specific assumption you're making in case it matters some day.