1%% -*- mode: erlang; tab-width: 4; indent-tabs-mode: 1; st-rulers: [70] -*- 2%% vim: ts=4 sw=4 ft=erlang noet 3-module(jose_jwa_pkcs1_props). 4 5-include_lib("public_key/include/public_key.hrl"). 6 7-include_lib("proper/include/proper.hrl"). 8 9% -compile(export_all). 10 11digest_type() -> oneof([md5, sha, sha224, sha256, sha384, sha512, {hmac, md5, <<>>}, {hmac, sha, <<>>}, {hmac, sha224, <<>>}, {hmac, sha256, <<>>}, {hmac, sha384, <<>>}, {hmac, sha512, <<>>}]). 12pkcs1_digest() -> oneof([md5, sha, sha256, sha384, sha512]). 13salt_size() -> non_neg_integer(). 14modulus_size() -> integer(1024, 1280). % integer(256, 8192) | pos_integer(). 15exponent_size() -> return(65537). % pos_integer(). 16 17rsa_keypair(ModulusSize) -> 18 ?LET(ExponentSize, 19 exponent_size(), 20 begin 21 case public_key:generate_key({rsa, ModulusSize, ExponentSize}) of 22 PrivateKey=#'RSAPrivateKey'{modulus=Modulus, publicExponent=PublicExponent} -> 23 {PrivateKey, #'RSAPublicKey'{modulus=Modulus, publicExponent=PublicExponent}} 24 end 25 end). 26 27%%==================================================================== 28%% RSAES-OAEP 29%%==================================================================== 30 31rsaes_oaep_encryptor_gen() -> 32 ?LET({DigestType, ModulusSize, PlainText}, 33 ?SUCHTHAT({DigestType, ModulusSize, PlainText}, 34 {digest_type(), modulus_size(), binary()}, 35 ModulusSize >= ((byte_size(do_hash(DigestType, <<>>)) * 2 + 2 + byte_size(PlainText)) * 8)), 36 {rsa_keypair(ModulusSize), ModulusSize, DigestType, PlainText}). 37 38rsaes_oaep_encryptor_with_label_gen() -> 39 ?LET({DigestType, ModulusSize, PlainText}, 40 ?SUCHTHAT({DigestType, ModulusSize, PlainText}, 41 {digest_type(), modulus_size(), binary()}, 42 ModulusSize >= ((byte_size(do_hash(DigestType, <<>>)) * 2 + 2 + byte_size(PlainText)) * 8)), 43 {rsa_keypair(ModulusSize), ModulusSize, DigestType, binary(), PlainText}). 44 45prop_rsaes_oaep_encrypt_and_decrypt() -> 46 ?FORALL({{PrivateKey, PublicKey}, _ModulusSize, DigestType, PlainText}, 47 rsaes_oaep_encryptor_gen(), 48 begin 49 {ok, CipherText} = jose_jwa_pkcs1:rsaes_oaep_encrypt(DigestType, PlainText, PublicKey), 50 PlainText =:= jose_jwa_pkcs1:rsaes_oaep_decrypt(DigestType, CipherText, PrivateKey) 51 end). 52 53prop_rsaes_oaep_encrypt_and_decrypt_with_label() -> 54 ?FORALL({{PrivateKey, PublicKey}, _ModulusSize, DigestType, Label, PlainText}, 55 rsaes_oaep_encryptor_with_label_gen(), 56 begin 57 {ok, CipherText} = jose_jwa_pkcs1:rsaes_oaep_encrypt(DigestType, PlainText, Label, PublicKey), 58 PlainText =:= jose_jwa_pkcs1:rsaes_oaep_decrypt(DigestType, CipherText, Label, PrivateKey) 59 end). 60 61%%==================================================================== 62%% RSAES-PKCS1-v1_5 63%%==================================================================== 64 65rsaes_pkcs1_encryptor_gen() -> 66 ?LET({ModulusSize, PlainText}, 67 ?SUCHTHAT({ModulusSize, PlainText}, 68 {modulus_size(), binary()}, 69 ModulusSize >= ((byte_size(PlainText) + 11) * 8)), 70 {rsa_keypair(ModulusSize), ModulusSize, PlainText}). 71 72prop_rsaes_pkcs1_encrypt_and_decrypt() -> 73 ?FORALL({{PrivateKey, PublicKey}, _ModulusSize, PlainText}, 74 rsaes_pkcs1_encryptor_gen(), 75 begin 76 {ok, CipherText} = jose_jwa_pkcs1:rsaes_pkcs1_encrypt(PlainText, PublicKey), 77 PlainText =:= jose_jwa_pkcs1:rsaes_pkcs1_decrypt(CipherText, PrivateKey) 78 end). 79 80%%==================================================================== 81%% RSASSA-PKCS1-v1_5 82%%==================================================================== 83 84rsassa_pkcs1_signer_gen() -> 85 ?LET({DigestType, ModulusSize}, 86 ?SUCHTHAT({DigestType, ModulusSize}, 87 {pkcs1_digest(), modulus_size()}, 88 ModulusSize >= (bit_size(do_hash(DigestType, <<>>)) * 3 + 16)), 89 {rsa_keypair(ModulusSize), ModulusSize, DigestType, binary()}). 90 91prop_rsassa_pkcs1_sign_and_verify() -> 92 ?FORALL({{PrivateKey, PublicKey}, _, DigestType, Message}, 93 rsassa_pkcs1_signer_gen(), 94 begin 95 {ok, Signature} = jose_jwa_pkcs1:rsassa_pkcs1_sign(DigestType, Message, PrivateKey), 96 jose_jwa_pkcs1:rsassa_pkcs1_verify(DigestType, Message, Signature, PublicKey) 97 end). 98 99%%==================================================================== 100%% RSASSA-PSS 101%%==================================================================== 102 103rsassa_pss_signer_gen() -> 104 ?LET({DigestType, ModulusSize}, 105 ?SUCHTHAT({DigestType, ModulusSize}, 106 {digest_type(), modulus_size()}, 107 ModulusSize >= (bit_size(do_hash(DigestType, <<>>)) * 2 + 16)), 108 {rsa_keypair(ModulusSize), ModulusSize, DigestType, binary()}). 109 110rsassa_pss_signer_with_salt_gen() -> 111 ?LET({DigestType, ModulusSize, SaltSize}, 112 ?SUCHTHAT({DigestType, ModulusSize, SaltSize}, 113 {digest_type(), modulus_size(), salt_size()}, 114 ModulusSize >= (bit_size(do_hash(DigestType, <<>>)) + (SaltSize * 8) + 16)), 115 {rsa_keypair(ModulusSize), ModulusSize, DigestType, binary(SaltSize), binary()}). 116 117prop_rsassa_pss_sign_and_verify() -> 118 ?FORALL({{PrivateKey, PublicKey}, _, DigestType, Message}, 119 rsassa_pss_signer_gen(), 120 begin 121 {ok, Signature} = jose_jwa_pkcs1:rsassa_pss_sign(DigestType, Message, PrivateKey), 122 jose_jwa_pkcs1:rsassa_pss_verify(DigestType, Message, Signature, PublicKey) 123 end). 124 125prop_rsassa_pss_sign_and_verify_with_salt() -> 126 ?FORALL({{PrivateKey, PublicKey}, _ModulusSize, DigestType, Salt, Message}, 127 rsassa_pss_signer_with_salt_gen(), 128 begin 129 {ok, Signature} = jose_jwa_pkcs1:rsassa_pss_sign(DigestType, Message, Salt, PrivateKey), 130 jose_jwa_pkcs1:rsassa_pss_verify(DigestType, Message, Signature, byte_size(Salt), PublicKey) 131 end). 132 133%%%------------------------------------------------------------------- 134%%% Internal functions 135%%%------------------------------------------------------------------- 136 137do_hash(DigestType, PlainText) when is_atom(DigestType) -> 138 crypto:hash(DigestType, PlainText); 139do_hash({hmac, DigestType, Key}, PlainText) -> 140 jose_crypto_compat:mac(hmac, DigestType, Key, PlainText). 141