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_jwk_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
11alg_map() ->
12	oneof([
13		#{ <<"alg">> => <<"RSA1_5">> },
14		#{ <<"alg">> => <<"RSA-OAEP">> },
15		#{ <<"alg">> => <<"RSA-OAEP-256">> },
16		#{ <<"alg">> => <<"A128KW">> },
17		#{ <<"alg">> => <<"A192KW">> },
18		#{ <<"alg">> => <<"A256KW">> },
19		#{ <<"alg">> => <<"dir">> },
20		#{ <<"alg">> => <<"ECDH-1PU">> },
21		#{ <<"alg">> => <<"ECDH-1PU+A128GCMKW">> },
22		#{ <<"alg">> => <<"ECDH-1PU+A192GCMKW">> },
23		#{ <<"alg">> => <<"ECDH-1PU+A256GCMKW">> },
24		#{ <<"alg">> => <<"ECDH-1PU+A128KW">> },
25		#{ <<"alg">> => <<"ECDH-1PU+A192KW">> },
26		#{ <<"alg">> => <<"ECDH-1PU+A256KW">> },
27		#{ <<"alg">> => <<"ECDH-1PU+C20PKW">> },
28		#{ <<"alg">> => <<"ECDH-1PU+XC20PKW">> },
29		#{ <<"alg">> => <<"ECDH-ES">> },
30		#{ <<"alg">> => <<"ECDH-ES+A128GCMKW">> },
31		#{ <<"alg">> => <<"ECDH-ES+A192GCMKW">> },
32		#{ <<"alg">> => <<"ECDH-ES+A256GCMKW">> },
33		#{ <<"alg">> => <<"ECDH-ES+A128KW">> },
34		#{ <<"alg">> => <<"ECDH-ES+A192KW">> },
35		#{ <<"alg">> => <<"ECDH-ES+A256KW">> },
36		#{ <<"alg">> => <<"ECDH-ES+C20PKW">> },
37		#{ <<"alg">> => <<"ECDH-ES+XC20PKW">> },
38		#{ <<"alg">> => <<"A128GCMKW">> },
39		#{ <<"alg">> => <<"A192GCMKW">> },
40		#{ <<"alg">> => <<"A256GCMKW">> },
41		?LET({P2C, P2S},
42			{integer(1, 256), binary()},
43			#{ <<"alg">> => <<"PBES2-HS256+A128GCMKW">>, <<"p2c">> => P2C, <<"p2s">> => jose_jwa_base64url:encode(P2S) }),
44		?LET({P2C, P2S},
45			{integer(1, 256), binary()},
46			#{ <<"alg">> => <<"PBES2-HS384+A192GCMKW">>, <<"p2c">> => P2C, <<"p2s">> => jose_jwa_base64url:encode(P2S) }),
47		?LET({P2C, P2S},
48			{integer(1, 256), binary()},
49			#{ <<"alg">> => <<"PBES2-HS512+A256GCMKW">>, <<"p2c">> => P2C, <<"p2s">> => jose_jwa_base64url:encode(P2S) }),
50		?LET({P2C, P2S},
51			{integer(1, 256), binary()},
52			#{ <<"alg">> => <<"PBES2-HS256+A128KW">>, <<"p2c">> => P2C, <<"p2s">> => jose_jwa_base64url:encode(P2S) }),
53		?LET({P2C, P2S},
54			{integer(1, 256), binary()},
55			#{ <<"alg">> => <<"PBES2-HS384+A192KW">>, <<"p2c">> => P2C, <<"p2s">> => jose_jwa_base64url:encode(P2S) }),
56		?LET({P2C, P2S},
57			{integer(1, 256), binary()},
58			#{ <<"alg">> => <<"PBES2-HS512+A256KW">>, <<"p2c">> => P2C, <<"p2s">> => jose_jwa_base64url:encode(P2S) }),
59		?LET({P2C, P2S},
60			{integer(1, 256), binary()},
61			#{ <<"alg">> => <<"PBES2-HS512+C20PKW">>, <<"p2c">> => P2C, <<"p2s">> => jose_jwa_base64url:encode(P2S) }),
62		?LET({P2C, P2S},
63			{integer(1, 256), binary()},
64			#{ <<"alg">> => <<"PBES2-HS512+XC20PKW">>, <<"p2c">> => P2C, <<"p2s">> => jose_jwa_base64url:encode(P2S) })
65	]).
66
67enc_map() ->
68	oneof([
69		#{ <<"enc">> => <<"A128CBC-HS256">> },
70		#{ <<"enc">> => <<"A192CBC-HS384">> },
71		#{ <<"enc">> => <<"A256CBC-HS512">> },
72		#{ <<"enc">> => <<"A128GCM">> },
73		#{ <<"enc">> => <<"A192GCM">> },
74		#{ <<"enc">> => <<"A256GCM">> },
75		#{ <<"enc">> => <<"C20P">> },
76		#{ <<"enc">> => <<"XC20P">> }
77	]).
78
79jwk_encryptor_gen() ->
80	?LET({ALGMap, ENCMap},
81		?SUCHTHAT({#{ <<"alg">> := _ALG }, #{ <<"enc">> := _ENC }},
82			{alg_map(), enc_map()},
83			true),
84		begin
85			ALG = maps:get(<<"alg">>, ALGMap),
86			ENC = maps:get(<<"enc">>, ENCMap),
87			JWE = jose_jwe:from_map(maps:merge(ENCMap, ALGMap)),
88			case {ALG, ENC} of
89				{<<"RSA", _/binary>>, _} ->
90					?LET({RSAPrivateKey, RSAPublicKey},
91						?LET(ModulusSize,
92							modulus_size(),
93							rsa_keypair(ModulusSize)),
94						begin
95							PrivateJWK = jose_jwk:from_key(RSAPrivateKey),
96							PublicJWK = jose_jwk:from_key(RSAPublicKey),
97							{{rsa, RSAPrivateKey, RSAPublicKey}, JWE, {PrivateJWK, PublicJWK}}
98						end);
99				{<<"A128KW">>, _} ->
100					K = crypto:strong_rand_bytes(16),
101					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
102				{<<"A192KW">>, _} ->
103					K = crypto:strong_rand_bytes(24),
104					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
105				{<<"A256KW">>, _} ->
106					K = crypto:strong_rand_bytes(32),
107					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
108				{<<"dir">>, <<"A128CBC-HS256">>} ->
109					K = crypto:strong_rand_bytes(32),
110					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
111				{<<"dir">>, <<"A192CBC-HS384">>} ->
112					K = crypto:strong_rand_bytes(48),
113					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
114				{<<"dir">>, <<"A256CBC-HS512">>} ->
115					K = crypto:strong_rand_bytes(64),
116					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
117				{<<"dir">>, <<"A128GCM">>} ->
118					K = crypto:strong_rand_bytes(16),
119					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
120				{<<"dir">>, <<"A192GCM">>} ->
121					K = crypto:strong_rand_bytes(24),
122					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
123				{<<"dir">>, <<"A256GCM">>} ->
124					K = crypto:strong_rand_bytes(32),
125					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
126				{<<"dir">>, <<"C20P">>} ->
127					K = crypto:strong_rand_bytes(32),
128					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
129				{<<"dir">>, <<"XC20P">>} ->
130					K = crypto:strong_rand_bytes(32),
131					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
132				{<<"ECDH-1PU", _/binary>>, _} ->
133					?LET(CurveId,
134						ec_curve(),
135						begin
136							VStaticKeypair = {VStaticSecret, VStaticPublic} = ec_keypair(CurveId),
137							UStaticKeypair = {UStaticSecret, UStaticPublic} = ec_keypair(CurveId),
138							UEphemeralKeypair = {UEphemeralSecret, UEphemeralPublic} = ec_keypair(CurveId),
139							VStaticSecretKey = jose_jwk:from_key(VStaticSecret),
140							VStaticPublicKey = jose_jwk:from_key(VStaticPublic),
141							UStaticSecretKey = jose_jwk:from_key(UStaticSecret),
142							UStaticPublicKey = jose_jwk:from_key(UStaticPublic),
143							UEphemeralSecretKey = jose_jwk:from_key(UEphemeralSecret),
144							UEphemeralPublicKey = jose_jwk:from_key(UEphemeralPublic),
145							{{ecdh_1pu, VStaticKeypair, UStaticKeypair, UEphemeralKeypair}, JWE, {{VStaticSecretKey, VStaticPublicKey}, {UStaticSecretKey, UStaticPublicKey}, {UEphemeralSecretKey, UEphemeralPublicKey}}}
146						end);
147				{<<"ECDH-ES", _/binary>>, _} ->
148					?LET(CurveId,
149						ec_curve(),
150						begin
151							AliceKeypair = {AlicePrivateKey, AlicePublicKey} = ec_keypair(CurveId),
152							BobKeypair = {BobPrivateKey, BobPublicKey} = ec_keypair(CurveId),
153							AlicePrivateJWK = jose_jwk:from_key(AlicePrivateKey),
154							AlicePublicJWK = jose_jwk:from_key(AlicePublicKey),
155							BobPrivateJWK = jose_jwk:from_key(BobPrivateKey),
156							BobPublicJWK = jose_jwk:from_key(BobPublicKey),
157							{{ecdh_es, AliceKeypair, BobKeypair}, JWE, {{AlicePrivateJWK, AlicePublicJWK}, {BobPrivateJWK, BobPublicJWK}}}
158						end);
159				{<<"A128GCMKW">>, _} ->
160					K = crypto:strong_rand_bytes(16),
161					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
162				{<<"A192GCMKW">>, _} ->
163					K = crypto:strong_rand_bytes(24),
164					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
165				{<<"A256GCMKW">>, _} ->
166					K = crypto:strong_rand_bytes(32),
167					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
168				{<<"C20PKW">>, _} ->
169					K = crypto:strong_rand_bytes(32),
170					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
171				{<<"XC20PKW">>, _} ->
172					K = crypto:strong_rand_bytes(32),
173					{K, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(K) })};
174				{<<"PBES2", _/binary>>, _} ->
175					?LET(Key,
176						binary(),
177						begin
178							Password = jose_jwa_base64url:encode(Key),
179							{Password, JWE, jose_jwk:from_map(#{ <<"kty">> => <<"oct">>, <<"k">> => jose_jwa_base64url:encode(Password) })}
180						end)
181			end
182		end).
183
184ec_curve() ->
185	oneof([
186		secp256r1,
187		secp384r1,
188		secp521r1,
189		x25519,
190		x448
191	]).
192
193ec_keypair(x25519) ->
194	SecretJWK = jose_jwk:generate_key({okp, 'X25519'}),
195	{_, SecretKey} = jose_jwk:to_key(SecretJWK),
196	{_, PublicKey} = jose_jwk:to_public_key(SecretJWK),
197	{SecretKey, PublicKey};
198ec_keypair(x448) ->
199	SecretJWK = jose_jwk:generate_key({okp, 'X448'}),
200	{_, SecretKey} = jose_jwk:to_key(SecretJWK),
201	{_, PublicKey} = jose_jwk:to_public_key(SecretJWK),
202	{SecretKey, PublicKey};
203ec_keypair(CurveId) ->
204	ECPrivateKey = #'ECPrivateKey'{parameters=ECParameters, publicKey=Octets0} = public_key:generate_key({namedCurve, pubkey_cert_records:namedCurves(CurveId)}),
205	Octets = case Octets0 of
206		{_, Octets1} ->
207			Octets1;
208		_ ->
209			Octets0
210	end,
211	ECPoint = #'ECPoint'{point=Octets},
212	ECPublicKey = {ECPoint, ECParameters},
213	{ECPrivateKey, ECPublicKey}.
214
215modulus_size()  -> integer(1048, 1280). % integer(256, 8192) | pos_integer().
216exponent_size() -> return(65537).   % pos_integer().
217
218rsa_keypair(ModulusSize) ->
219	?LET(ExponentSize,
220		exponent_size(),
221		begin
222			case public_key:generate_key({rsa, ModulusSize, ExponentSize}) of
223				PrivateKey=#'RSAPrivateKey'{modulus=Modulus, publicExponent=PublicExponent} ->
224					{PrivateKey, #'RSAPublicKey'{modulus=Modulus, publicExponent=PublicExponent}}
225			end
226		end).
227
228prop_encrypt_and_decrypt() ->
229	?FORALL({Keys, JWE, JWKs, PlainText},
230		?LET({Keys, JWE, JWKs},
231			jwk_encryptor_gen(),
232			{Keys, JWE, JWKs, binary()}),
233		begin
234			case {Keys, JWKs} of
235				{{ecdh_1pu, _, _, _}, {{VStaticSecretKey, VStaticPublicKey}, {UStaticSecretKey, UStaticPublicKey}, {UEphemeralSecretKey, UEphemeralPublicKey}}} ->
236					JWEMap = jose_jwe:to_map(JWE),
237					Encrypted = jose_jwk:box_encrypt_ecdh_1pu(PlainText, JWEMap, VStaticPublicKey, UStaticSecretKey, UEphemeralSecretKey),
238					CompactEncrypted = jose_jwe:compact(Encrypted),
239					Decrypted = {_, NewJWE} = jose_jwk:box_decrypt_ecdh_1pu(Encrypted, UStaticPublicKey, VStaticSecretKey),
240					{PlainText, NewJWE} =:= Decrypted
241					andalso {PlainText, NewJWE} =:= jose_jwe:block_decrypt({UStaticPublicKey, VStaticSecretKey, UEphemeralPublicKey}, CompactEncrypted);
242				{{ecdh_es, _, _}, {{AlicePrivateJWK, _AlicePublicJWK}, {BobPrivateJWK, BobPublicJWK}}} ->
243					JWEMap = jose_jwe:to_map(JWE),
244					Encrypted = jose_jwk:box_encrypt_ecdh_es(PlainText, JWEMap, BobPublicJWK, AlicePrivateJWK),
245					CompactEncrypted = jose_jwe:compact(Encrypted),
246					Decrypted = {_, NewJWE} = jose_jwk:box_decrypt_ecdh_es(Encrypted, BobPrivateJWK),
247					{PlainText, NewJWE} =:= Decrypted
248					andalso {PlainText, NewJWE} =:= jose_jwk:block_decrypt(CompactEncrypted, BobPrivateJWK);
249				{{rsa, _, _}, {PrivateJWK, PublicJWK}} ->
250					Encrypted = jose_jwk:block_encrypt(PlainText, JWE, PublicJWK),
251					CompactEncrypted = jose_jwe:compact(Encrypted),
252					Decrypted = {_, NewJWE} = jose_jwk:block_decrypt(Encrypted, PrivateJWK),
253					{PlainText, NewJWE} =:= Decrypted
254					andalso {PlainText, NewJWE} =:= jose_jwk:block_decrypt(CompactEncrypted, PrivateJWK);
255				{_, JWK} ->
256					Encrypted = jose_jwk:block_encrypt(PlainText, JWE, JWK),
257					CompactEncrypted = jose_jwe:compact(Encrypted),
258					Decrypted = {_, NewJWE} = jose_jwk:block_decrypt(Encrypted, JWK),
259					{PlainText, NewJWE} =:= Decrypted
260					andalso {PlainText, NewJWE} =:= jose_jwk:block_decrypt(CompactEncrypted, JWK)
261			end
262		end).
263