Post #4756294 · Elektrine

2026-09-18 22:08 UTC

@alwayscurious@infosec.exchange @mei@donotsta.re these proof types serve slightly different purposes: reduction proofs are very useful when constructing cryptographic primitives. I.e. you want to show that AES-CTR is IND-CPA secure as long as AES is a secure PRP. The direct proofs you mentioned are usually used to prove protocols secure, using the properties that the primitives are shown to have to construct an interaction that is secure, as long as the components are secure. They usually could also be written as reduction proofs (assume the protocol is broken by attacker A. Since we verified the certificate, this means the certificate has a valid signature without the adversary having access to the private key, we can construct an EUF-CMA attacker A' that calls A, simulating the protocol to it using its oracle that will now win its attack game). It's just that for a protocol analysis this type of reduction proof is usually overkill and doesn't convey information, so it's merely implied and left to the reader.

Replies (1)

@sophieschmieg@infosec.exchange 2026-09-18 22:18

@alwayscurious@infosec.exchange @mei@donotsta.re one important thing to know about mathematics is that there are two layers to every problem: how to find the solution and how to formalize the solution. Finding the solution usually involves steps that are omitted when writing up the solution as a formal proof, but are just as important to develop. Oftentimes, the formal write-up ends up being the inverse of what you actually did to find the solution in the first place: you start out exploring your problem and noting necessary and sufficient conditions for it. Then you start looking at those conditions and try to find necessary and sufficient conditions for these etc. But when writing up the proof, you start with your collection of lemmas, and only move to prove the main theorem once you have all your preconditions sorted out. Reduction proofs follow a similar pattern: when actually doing the research, you don't start with "assuming I have an attack on my problem, how does this attack my building blocks", but you start with "what properties do I need and what building blocks provide those", and only when you have a construction that actually works you move to write it up as a formal reduction proof, following the breadcrumbs you got when constructing your protocol/primitive. The formal step is still very important, especially for primitives, as it ensures that nothing slipped through. In protocols you can use things like universal composability instead of reduction at times, making the proof look more natural.

Open ##4756293