Reusing a one-bit encryption pad — definitions

Lax755887.ReusedKey · concepts/Lax755887/ReusedKey.lean · lax-755887

definition

Loading review…

Equal marginal distributions do not determine a joint distribution. The composition contract deliberately omits a condition on joint randomness.

Concept map

1 concept; 3 descendants hidden

100%

Proven claimOpen claimDefinitionThis conceptRelated conceptA → B: B builds on A

1	import Mathlib
2
3	/-!
4	---
5	title: Reusing a one-bit encryption pad — definitions
6	type: definition
7	---
8	Equal marginal distributions do not determine a joint distribution. The composition contract deliberately omits a condition on joint randomness.
9	-/
10
11	namespace Lax755887.ReusedKey
12
13	def probability (event : Bool → Bool) : ℚ :=
14	((if event false then 1 else 0) + (if event true then 1 else 0)) / 2
15
16	def SameLaw {α : Type} (X Y : Bool → α) : Prop :=
17	∀ test : α → Bool, probability (fun k => test (X k)) = probability (fun k => test (Y k))
18
19	def transcript (secret key : Bool) : Bool × Bool := (key, Bool.xor key secret)
20
21	def success (guess : Bool × Bool → Bool) : ℚ :=
22	(probability (fun k => !(guess (transcript false k))) +
23	probability (fun k => guess (transcript true k))) / 2
24
25	end Lax755887.ReusedKey
26

Builds on

none

Used by

From Mathlib

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive