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