RSA One-Way Assumption

This file defines the RSA one-wayness assumption at the abstract CryptoWord W level, used for the FDH signature scheme.

RSA Game

The RSA game captures the difficulty of inverting the RSA function:

• Challenger samples RSA key pair and random y ∈ Z_N*
• Adversary must find x such that rsa(pk, x) = y

Cross-Validation

Property	This file	Textbook
Game structure	RSA_Game_Real	Boneh-Shoup Def. 10.2
Advantage	Advantage(Real, Ideal)	Pr[RSAadv]
Formulation	Inversion game	Standard one-wayness

Equivalent formalizations:

• EasyCrypt: RSA theory
• CryptoVerif: OW(f, inv, key) macro

References

• Rivest, Shamir, Adleman. A Method for Obtaining Digital Signatures and Public-Key Cryptosystems. CACM 1978.
• Boneh & Shoup, A Graduate Course in Applied Cryptography, §10.3, Def. 10.2
• Blanchet, Pointcheval. Automated Security Proofs with Sequences of Games. CRYPTO 2006.

RSA Definition

structure CatCrypt.Crypto.Assumptions.RSADef (W : Type) [SampleableType W] : Type

Abstract RSA definition, parametric over SampleableType W.

• rsa pk x → y (the RSA function under public key)
• rsa_inv sk y → x (the RSA inverse under secret key)
• keygen → (sk, pk)

• rsa : W → W → W

  RSA function: (public_key, preimage) → image

• rsa_inv : W → W → W

  RSA inverse: (secret_key, image) → preimage

• keygen : Core.SPComp (W × W)

  RSA key generation: (secret_key, public_key)

• keygen_isPure : self.keygen.IsPure

  Key generation is heap-independent

RSA Games

@[reducible, inline]

abbrev CatCrypt.Crypto.Assumptions.RSA_Adversary (W : Type) : Type

Type of RSA adversary: receives (pk, y) and must find x with rsa(pk, x) = y.

Equations

• CatCrypt.Crypto.Assumptions.RSA_Adversary W = (W → W → CatCrypt.Core.SPComp W)

noncomputable def CatCrypt.Crypto.Assumptions.RSA_Game_Real {W : Type} [SampleableType W] (D : RSADef W) (A : RSA_Adversary W) : Core.SPComp Bool

RSA inversion game (real): adversary tries to invert rsa(pk, ·).

Returns true if the adversary successfully inverts.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCrypt.Crypto.Assumptions.RSA_Game_Ideal {W : Type} [SampleableType W] (D : RSADef W) (A : RSA_Adversary W) : Core.SPComp Bool

RSA inversion game (ideal): always returns false.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CatCrypt.Crypto.Assumptions.RSA_Advantage {W : Type} [SampleableType W] (D : RSADef W) (A : RSA_Adversary W) : ENNReal

RSA advantage: distinguishing advantage for the inversion game.

Equations

• CatCrypt.Crypto.Assumptions.RSA_Advantage D A = CatCrypt.Crypto.Advantage (CatCrypt.Crypto.Assumptions.RSA_Game_Real D A) (CatCrypt.Crypto.Assumptions.RSA_Game_Ideal D A)

IsPure Proofs

theorem CatCrypt.Crypto.Assumptions.RSA_Game_Real_isPure {W : Type} [SampleableType W] (D : RSADef W) (A : RSA_Adversary W) (hA : ∀ (x y : W), (A x y).IsPure) : (RSA_Game_Real D A).IsPure