Post #4756295 · Elektrine

2026-09-18 21:49 UTC

@mei@donotsta.re @sophieschmieg@infosec.exchange By “direct proof”, I mean “not a proof by contradiction”. Security reductions are proofs by contradiction: you assume that there is an attacker who can break the protocol, and show that they can solve a hard problem. Since we assume that the hard problem is not solvable, such an attacker cannot exist. A direct proof would be something like, “The server signed the handshake transcript, and we verified the server’s certificate is authentic. Therefore, the ciphertext we got is the one sent by the server, which means that decapsulating it produces a secret only we and the server know. Replay attacks aren’t possible because both the client and the server include a random value in the transcript, and the whole transcript is hashed, so nobody can mix and match handshakes.”

Replies (1)

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

@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.

Open ##4756294