Version 1.11.7 (2024-04-07)

* Security Patches
  * [CVE-2023-50966](https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2023-50966): Add `jose:pbes2_count_maximum/0`.  By default, the maximum iterations are set to 10,000 and it will raise an error if `p2c` is larger than this value.
* Changes
  * Declare Poison as an optional dependency, thanks to [@lnikkila][https://github.com/lnikkila]; see [#144](#144).
  * Ensure `jiffy:encode/1` returns a binary, thanks to [@ssepml](https://github.com/ssepml); see [#145](#145).
  * Various type spec additions and dialyzer/dialyxir integrations, thanks to [@whatyouhide](https://github.com/whatyouhide) and [@maennchen](https://github.com/maennchen).
  * Doc updates and fixes, thanks to [@aymanosman](https://github.com/aymanosman) and [@adamu](https://github.com/adamu); see [#158](#158) and [#159](#159).

Author: potatosalad

CHANGELOG.md

@@ -1,5 +1,15 @@
 # Changelog
 
+## 1.11.7 (2024-04-07)
+
+* Security Patches
+  * [CVE-2023-50966](https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2023-50966): Add `jose:pbes2_count_maximum/0`.  By default, the maximum iterations are set to 10,000 and it will raise an error if `p2c` is larger than this value.
+* Changes
+  * Declare Poison as an optional dependency, thanks to [@lnikkila][https://github.com/lnikkila]; see [#144](https://github.com/potatosalad/erlang-jose/pull/144).
+  * Ensure `jiffy:encode/1` returns a binary, thanks to [@ssepml](https://github.com/ssepml); see [#145](https://github.com/potatosalad/erlang-jose/pull/145).
+  * Various type spec additions and dialyzer/dialyxir integrations, thanks to [@whatyouhide](https://github.com/whatyouhide) and [@maennchen](https://github.com/maennchen).
+  * Doc updates and fixes, thanks to [@aymanosman](https://github.com/aymanosman) and [@adamu](https://github.com/adamu); see [#158](https://github.com/potatosalad/erlang-jose/pull/158) and [#159](https://github.com/potatosalad/erlang-jose/pull/159).
+
 ## 1.11.6 (2023-07-18)
 
 * Fixes

Makefile

@@ -1,6 +1,6 @@
 PROJECT = jose
 PROJECT_DESCRIPTION = JSON Object Signing and Encryption (JOSE) for Erlang and Elixir.
-PROJECT_VERSION = 1.11.6
+PROJECT_VERSION = 1.11.7
 
 TEST_DEPS = jiffy jsone jsx libdecaf libsodium ojson proper thoas
 

src/jose.app.src

@@ -2,7 +2,7 @@
 %% vim: ts=4 sw=4 ft=erlang noet
 {application, jose, [
 	{description, "JSON Object Signing and Encryption (JOSE) for Erlang and Elixir."},
-	{vsn, "1.11.6"},
+	{vsn, "1.11.7"},
 	{id, "git"},
 	{mod, {'jose_app', []}},
 	{registered, []},
@@ -17,6 +17,9 @@
 	{maintainers, ["Andrew Bennett"]},
 	{licenses, ["MIT"]},
 	{links, [{"Github", "https://github.com/potatosalad/erlang-jose"}]},
-	{env, [{crypto_fallback, true}]}
+	{env, [
+		{crypto_fallback, true},
+		{pbes2_count_maximum, 10000}
+	]}
 ]}.
 

src/jose.erl

@@ -23,6 +23,8 @@
 -export([encode/1]).
 -export([json_module/0]).
 -export([json_module/1]).
+-export([pbes2_count_maximum/0]).
+-export([pbes2_count_maximum/1]).
 -export([sha3_module/0]).
 -export([sha3_module/1]).
 -export([unsecured_signing/0]).
@@ -84,17 +86,27 @@ json_module() ->
 json_module(JSONModule) when is_atom(JSONModule) ->
 	?MAYBE_START_JOSE(jose_server:json_module(JSONModule)).
 
+-spec pbes2_count_maximum() -> non_neg_integer().
+pbes2_count_maximum() ->
+	?MAYBE_START_JOSE(ets:lookup_element(?TAB, pbes2_count_maximum, 2)).
+
+-spec pbes2_count_maximum(PBES2CountMaximum) -> ok when PBES2CountMaximum :: non_neg_integer().
+pbes2_count_maximum(PBES2CountMaximum) when is_integer(PBES2CountMaximum) andalso PBES2CountMaximum >= 0 ->
+	?MAYBE_START_JOSE(jose_server:pbes2_count_maximum(PBES2CountMaximum)).
+
 sha3_module() ->
 	?MAYBE_START_JOSE(ets:lookup_element(?TAB, sha3_module, 2)).
 
 sha3_module(SHA3Module) when is_atom(SHA3Module) ->
 	?MAYBE_START_JOSE(jose_server:sha3_module(SHA3Module)).
 
+-spec unsecured_signing() -> boolean().
 unsecured_signing() ->
-	jose_jwa:unsecured_signing().
+	?MAYBE_START_JOSE(ets:lookup_element(?TAB, unsecured_signing, 2)).
 
-unsecured_signing(Boolean) when is_boolean(Boolean) ->
-	jose_jwa:unsecured_signing(Boolean).
+-spec unsecured_signing(UnsecuredSigning) -> ok when UnsecuredSigning :: boolean().
+unsecured_signing(UnsecuredSigning) when is_boolean(UnsecuredSigning) ->
+	?MAYBE_START_JOSE(jose_server:unsecured_signing(UnsecuredSigning)).
 
 xchacha20_poly1305_module() ->
 	?MAYBE_START_JOSE(ets:lookup_element(?TAB, xchacha20_poly1305_module, 2)).

src/jose_server.erl

@@ -22,7 +22,9 @@
 -export([curve25519_module/1]).
 -export([curve448_module/1]).
 -export([json_module/1]).
+-export([pbes2_count_maximum/1]).
 -export([sha3_module/1]).
+-export([unsecured_signing/1]).
 -export([xchacha20_poly1305_module/1]).
 
 %% gen_server callbacks
@@ -72,9 +74,17 @@ curve448_module(Curve448Module) when is_atom(Curve448Module) ->
 json_module(JSONModule) when is_atom(JSONModule) ->
 	gen_server:call(?SERVER, {json_module, JSONModule}).
 
+-spec pbes2_count_maximum(PBES2CountMaximum) -> ok when PBES2CountMaximum :: non_neg_integer().
+pbes2_count_maximum(PBES2CountMaximum) when is_integer(PBES2CountMaximum) andalso PBES2CountMaximum >= 0 ->
+	gen_server:call(?SERVER, {pbes2_count_maximum, PBES2CountMaximum}).
+
 sha3_module(SHA3Module) when is_atom(SHA3Module) ->
 	gen_server:call(?SERVER, {sha3_module, SHA3Module}).
 
+-spec unsecured_signing(UnsecuredSigning) -> ok when UnsecuredSigning :: boolean().
+unsecured_signing(UnsecuredSigning) when is_boolean(UnsecuredSigning) ->
+	gen_server:call(?SERVER, {unsecured_signing, UnsecuredSigning}).
+
 xchacha20_poly1305_module(XChaCha20Poly1305Module) when is_atom(XChaCha20Poly1305Module) ->
 	gen_server:call(?SERVER, {xchacha20_poly1305_module, XChaCha20Poly1305Module}).
 
@@ -114,10 +124,20 @@ handle_call({json_module, M}, _From, State) ->
 	JSONModule = check_json_module(M),
 	true = ets:insert(?TAB, {json_module, JSONModule}),
 	{reply, ok, State};
+handle_call({pbes2_count_maximum, PBES2CountMaximum}, _From, State) when is_integer(PBES2CountMaximum) andalso PBES2CountMaximum >= 0 ->
+	true = ets:insert(?TAB, {pbes2_count_maximum, PBES2CountMaximum}),
+	{reply, ok, State};
 handle_call({sha3_module, M}, _From, State) ->
 	SHA3Module = check_sha3_module(M),
 	true = ets:insert(?TAB, {sha3_module, SHA3Module}),
 	{reply, ok, State};
+handle_call({unsecured_signing, UnsecuredSigning}, _From, State) when is_boolean(UnsecuredSigning) ->
+	true = ets:insert(?TAB, {unsecured_signing, UnsecuredSigning}),
+	_ = spawn(fun() ->
+		_ = catch jose_jwa:unsecured_signing(UnsecuredSigning),
+		exit(normal)
+	end),
+	{reply, ok, State};
 handle_call({xchacha20_poly1305_module, M}, _From, State) ->
 	XChaCha20Poly1305Module = check_xchacha20_poly1305_module(M),
 	Entries = lists:flatten(check_crypto(?CRYPTO_FALLBACK, [{xchacha20_poly1305_module, XChaCha20Poly1305Module}])),
@@ -149,8 +169,18 @@ code_change(_OldVsn, State, _Extra) ->
 
 %% @private
 support_check() ->
+	PBES2CountMaximum =
+		case application:get_env(jose, pbes2_count_maximum, 10000) of
+			V1 when is_integer(V1) andalso V1 >= 0 ->
+				V1
+		end,
+	UnsecuredSigning =
+		case application:get_env(jose, unsecured_signing, false) of
+			V2 when is_boolean(V2) ->
+				V2
+		end,
 	Fallback = ?CRYPTO_FALLBACK,
-	Entries = lists:flatten(lists:foldl(fun(Check, Acc) ->
+	Entries1 = lists:flatten(lists:foldl(fun(Check, Acc) ->
 		Check(Fallback, Acc)
 	end, [], [
 		fun check_sha3/2,
@@ -163,8 +193,13 @@ support_check() ->
 		fun check_crypto/2,
 		fun check_public_key/2
 	])),
+	Entries2 = [
+		{pbes2_count_maximum, PBES2CountMaximum},
+		{unsecured_signing, UnsecuredSigning}
+		| Entries1
+	],
 	true = ets:delete_all_objects(?TAB),
-	true = ets:insert(?TAB, Entries),
+	true = ets:insert(?TAB, Entries2),
 	ok.
 
 %%%-------------------------------------------------------------------

src/jwa/jose_jwa.erl

@@ -380,7 +380,7 @@ supports() ->
 	].
 
 unsecured_signing() ->
-	application:get_env(jose, unsecured_signing, false).
+	jose:unsecured_signing().
 
 unsecured_signing(Boolean) when is_boolean(Boolean) ->
 	application:set_env(jose, unsecured_signing, Boolean),

src/jwe/jose_jwe_alg_pbes2.erl

@@ -23,6 +23,7 @@
 -export([key_encrypt/3]).
 -export([next_cek/3]).
 %% API
+-export([format_error/2]).
 -export([hmac_supported/0]).
 -export([wrap_supported/0]).
 
@@ -99,22 +100,22 @@ key_decrypt(Password, {_ENCModule, _ENC, EncryptedKey}, #jose_jwe_alg_pbes2{hmac
 		when is_binary(Password)
 		andalso is_binary(IV)
 		andalso is_binary(TAG) ->
-	{ok, DerivedKey} = jose_jwa_pkcs5:pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
+	{ok, DerivedKey} = pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
 	jose_jwa:block_decrypt({aes_gcm, Bits}, DerivedKey, IV, {<<>>, EncryptedKey, TAG});
 key_decrypt(Password, {_ENCModule, _ENC, EncryptedKey}, #jose_jwe_alg_pbes2{hmac=HMAC, salt=Salt, iter=Iterations, wrap=aes_kw, bits=Bits}) when is_binary(Password) ->
-	{ok, DerivedKey} = jose_jwa_pkcs5:pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
+	{ok, DerivedKey} = pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
 	jose_jwa_aes_kw:unwrap(EncryptedKey, DerivedKey);
 key_decrypt(Password, {_ENCModule, _ENC, EncryptedKey}, #jose_jwe_alg_pbes2{hmac=HMAC, salt=Salt, iter=Iterations, wrap=c20p_kw, bits=Bits, iv=IV, tag=TAG})
 		when is_binary(Password)
 		andalso is_binary(IV)
 		andalso is_binary(TAG) ->
-	{ok, DerivedKey} = jose_jwa_pkcs5:pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
+	{ok, DerivedKey} = pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
 	jose_jwa:block_decrypt({chacha20_poly1305, Bits}, DerivedKey, IV, {<<>>, EncryptedKey, TAG});
 key_decrypt(Password, {_ENCModule, _ENC, EncryptedKey}, #jose_jwe_alg_pbes2{hmac=HMAC, salt=Salt, iter=Iterations, wrap=xc20p_kw, bits=Bits, iv=IV, tag=TAG})
 		when is_binary(Password)
 		andalso is_binary(IV)
 		andalso is_binary(TAG) ->
-	{ok, DerivedKey} = jose_jwa_pkcs5:pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
+	{ok, DerivedKey} = pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
 	jose_jwa:block_decrypt({xchacha20_poly1305, Bits}, DerivedKey, IV, {<<>>, EncryptedKey, TAG});
 key_decrypt(#jose_jwk{kty={KTYModule, KTY}}, EncryptedKey, JWEPBES2=#jose_jwe_alg_pbes2{}) ->
 	key_decrypt(KTYModule:derive_key(KTY), EncryptedKey, JWEPBES2).
@@ -131,23 +132,23 @@ key_encrypt(Password, DecryptedKey, JWEPBES2=#jose_jwe_alg_pbes2{hmac=HMAC, salt
 		andalso is_binary(Salt)
 		andalso is_integer(Iterations)
 		andalso is_binary(IV) ->
-	{ok, DerivedKey} = jose_jwa_pkcs5:pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
+	{ok, DerivedKey} = pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
 	{CipherText, CipherTag} = jose_jwa:block_encrypt({aes_gcm, Bits}, DerivedKey, IV, {<<>>, DecryptedKey}),
 	{CipherText, JWEPBES2#jose_jwe_alg_pbes2{ tag = CipherTag }};
 key_encrypt(Password, DecryptedKey, JWEPBES2=#jose_jwe_alg_pbes2{hmac=HMAC, salt=Salt, iter=Iterations, wrap=aes_kw, bits=Bits})
 		when is_binary(Password)
 		andalso is_binary(DecryptedKey)
 		andalso is_binary(Salt)
 		andalso is_integer(Iterations) ->
-	{ok, DerivedKey} = jose_jwa_pkcs5:pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
+	{ok, DerivedKey} = pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
 	{jose_jwa_aes_kw:wrap(DecryptedKey, DerivedKey), JWEPBES2};
 key_encrypt(Password, DecryptedKey, JWEPBES2=#jose_jwe_alg_pbes2{hmac=HMAC, salt=Salt, iter=Iterations, wrap=c20p_kw, bits=Bits, iv=IV})
 		when is_binary(Password)
 		andalso is_binary(DecryptedKey)
 		andalso is_binary(Salt)
 		andalso is_integer(Iterations)
 		andalso is_binary(IV) ->
-	{ok, DerivedKey} = jose_jwa_pkcs5:pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
+	{ok, DerivedKey} = pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
 	{CipherText, CipherTag} = jose_jwa:block_encrypt({chacha20_poly1305, Bits}, DerivedKey, IV, {<<>>, DecryptedKey}),
 	{CipherText, JWEPBES2#jose_jwe_alg_pbes2{ tag = CipherTag }};
 key_encrypt(Password, DecryptedKey, JWEPBES2=#jose_jwe_alg_pbes2{hmac=HMAC, salt=Salt, iter=Iterations, wrap=xc20p_kw, bits=Bits, iv=IV})
@@ -156,7 +157,7 @@ key_encrypt(Password, DecryptedKey, JWEPBES2=#jose_jwe_alg_pbes2{hmac=HMAC, salt
 		andalso is_binary(Salt)
 		andalso is_integer(Iterations)
 		andalso is_binary(IV) ->
-	{ok, DerivedKey} = jose_jwa_pkcs5:pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
+	{ok, DerivedKey} = pbkdf2({hmac, HMAC}, Password, Salt, Iterations, (Bits div 8) + (Bits rem 8)),
 	{CipherText, CipherTag} = jose_jwa:block_encrypt({xchacha20_poly1305, Bits}, DerivedKey, IV, {<<>>, DecryptedKey}),
 	{CipherText, JWEPBES2#jose_jwe_alg_pbes2{ tag = CipherTag }};
 key_encrypt(Password, DecryptedKey, JWEPBES2=#jose_jwe_alg_pbes2{wrap=aes_gcm_kw, iv=undefined}) when is_binary(Password) ->
@@ -175,6 +176,12 @@ next_cek(_Key, {ENCModule, ENC}, ALG=#jose_jwe_alg_pbes2{}) ->
 %% API functions
 %%====================================================================
 
+-spec format_error(dynamic(), dynamic()) -> dynamic().
+format_error(_Reason, [{_M, _F, _As, Info} | _]) ->
+    ErrorInfo = proplists:get_value(error_info, Info, #{}),
+    ErrorDescription1 = maps:get(cause, ErrorInfo),
+    ErrorDescription1.
+
 hmac_supported() ->
 	[sha256, sha384, sha512].
 
@@ -197,6 +204,21 @@ from_map_pbes2(F=#{ <<"tag">> := TAG }, H) ->
 from_map_pbes2(F, H) ->
 	{H, F}.
 
+%% @private
+pbkdf2(Mac, Password, Salt, Iterations, DerivedKeyLen) ->
+	PBES2CountMaximum = jose:pbes2_count_maximum(),
+	case PBES2CountMaximum < Iterations of
+		false ->
+			jose_jwa_pkcs5:pbkdf2(Mac, Password, Salt, Iterations, DerivedKeyLen);
+		true ->
+			erlang:error(badarg, [Mac, <<"REDACTED">>, Salt, Iterations, DerivedKeyLen], [
+				{error_info, #{
+					module => ?MODULE,
+					cause => #{4 => lists:flatten(io_lib:format("maximum PBES2 iterations is set to ~w, but ~w was attempted (see jose:pbes2_count_maximum/0)", [PBES2CountMaximum, Iterations]))}
+				}}
+			])
+	end.
+
 %% @private
 to_map_pbes2(F, H=#jose_jwe_alg_pbes2{ iter = P2C }) when is_integer(P2C) ->
 	to_map_pbes2(F#{ <<"p2c">> => P2C }, H#jose_jwe_alg_pbes2{ iter = undefined });

test/jose_jwe_SUITE.erl

@@ -27,6 +27,7 @@
 -export([alg_ecdh_1pu_key_encrypt_and_key_decrypt/1]).
 -export([alg_ecdh_es_from_map_and_to_map/1]).
 -export([alg_ecdh_es_key_encrypt_and_key_decrypt/1]).
+-export([alg_pbes2_cve_2023_50966/1]).
 -export([alg_pbes2_from_map_and_to_map/1]).
 -export([alg_pbes2_key_encrypt_and_key_decrypt/1]).
 -export([alg_rsa_from_map_and_to_map/1]).
@@ -53,6 +54,7 @@ all() ->
 		{group, jose_jwe_alg_pbes2},
 		{group, jose_jwe_alg_rsa},
 		{group, jose_jwe_alg_xc20p_kw},
+		{group, jose_jwe_cve},
 		{group, jose_jwe_enc_aes},
 		{group, jose_jwe_enc_c20p},
 		{group, jose_jwe_enc_xc20p},
@@ -69,6 +71,9 @@ groups() ->
 			alg_c20p_kw_from_map_and_to_map,
 			alg_c20p_kw_key_encrypt_and_key_decrypt
 		]},
+		{jose_jwe_cve, [shuffle], [
+			alg_pbes2_cve_2023_50966
+		]},
 		{jose_jwe_alg_dir, [parallel], [
 			alg_dir_from_map_and_to_map,
 			alg_dir_key_decrypt,
@@ -195,6 +200,11 @@ alg_ecdh_es_key_encrypt_and_key_decrypt(Config) ->
 		jose_jwe_alg_ecdh_es_props:prop_key_encrypt_and_key_decrypt(),
 		Config).
 
+alg_pbes2_cve_2023_50966(Config) ->
+	ct_property_test:quickcheck(
+		jose_jwe_alg_pbes2_props:prop_cve_2023_50966(),
+		Config).
+
 alg_pbes2_from_map_and_to_map(Config) ->
 	ct_property_test:quickcheck(
 		jose_jwe_alg_pbes2_props:prop_from_map_and_to_map(),

test/jose_jws_SUITE.erl

@@ -76,7 +76,9 @@ groups() ->
 init_per_suite(Config) ->
 	application:set_env(jose, crypto_fallback, true),
 	application:set_env(jose, unsecured_signing, true),
-	_ = application:ensure_all_started(jose),
+	{ok, _} = application:ensure_all_started(jose),
+	ok = jose:crypto_fallback(true),
+	ok = jose:unsecured_signing(true),
 	ct_property_test:init_per_suite(Config).
 
 end_per_suite(_Config) ->

test/property_test/jose_jwe_alg_pbes2_props.erl

@@ -61,6 +61,52 @@ jwk_jwe_gen() ->
 		jwk_jwe_maps(),
 		{Key, jose_jwk:from_map(JWKMap), jose_jwe:from_map(JWEMap)}).
 
+prop_cve_2023_50966() ->
+	?FORALL({_Key, JWK, BaseJWE, PBES2CountMaximum},
+		?LET({{Key, JWK, BaseJWE}, PBES2CountMaximum},
+			{jwk_jwe_gen(), range(2, 100)},
+			{Key, oneof([Key, JWK]), BaseJWE, PBES2CountMaximum}),
+		begin
+			OriginalPBES2CountMaximum = jose:pbes2_count_maximum(),
+			try jose:pbes2_count_maximum(PBES2CountMaximum) of
+				ok ->
+					LesserJWE = jose_jwe:merge(BaseJWE, #{<<"p2c">> => PBES2CountMaximum - 1}),
+					MaximumJWE = jose_jwe:merge(BaseJWE, #{<<"p2c">> => PBES2CountMaximum}),
+					GreaterJWE = jose_jwe:merge(BaseJWE, #{<<"p2c">> => PBES2CountMaximum + 1}),
+					{LesserDecKey1, LesserDecJWE} = jose_jwe:next_cek(JWK, LesserJWE),
+					{LesserEncKey, LesserEncJWE} = jose_jwe:key_encrypt(JWK, LesserDecKey1, LesserDecJWE),
+					LesserDecKey2 = jose_jwe:key_decrypt(JWK, LesserEncKey, LesserEncJWE),
+					{MaximumDecKey1, MaximumDecJWE} = jose_jwe:next_cek(JWK, MaximumJWE),
+					{MaximumEncKey, MaximumEncJWE} = jose_jwe:key_encrypt(JWK, MaximumDecKey1, MaximumDecJWE),
+					MaximumDecKey2 = jose_jwe:key_decrypt(JWK, MaximumEncKey, MaximumEncJWE),
+					{GreaterDecKey, GreaterDecJWE} = jose_jwe:next_cek(JWK, GreaterJWE),
+					GreaterEncResult =
+						try
+							jose_jwe:key_encrypt(JWK, GreaterDecKey, GreaterDecJWE)
+						catch
+							GreaterEncClass:GreaterEncReason ->
+								{GreaterEncClass, GreaterEncReason}
+						end,
+					{GreaterEncKey, GreaterEncJWE1} = jose_jwe:key_encrypt(JWK, GreaterDecKey, MaximumDecJWE),
+					GreaterEncJWE2 = jose_jwe:merge(GreaterEncJWE1, #{<<"p2c">> => 1000000000}),
+					GreaterDecResult =
+						try
+							jose_jwe:key_decrypt(JWK, GreaterEncKey, GreaterEncJWE2)
+						catch
+							GreaterDecClass:GreaterDecReason ->
+								{GreaterDecClass, GreaterDecReason}
+						end,
+					conjunction([
+						{lesser, LesserDecKey1 =:= LesserDecKey2},
+						{maximum, MaximumDecKey1 =:= MaximumDecKey2},
+						{greater_key_encrypt, {error, badarg} =:= GreaterEncResult},
+						{greater_key_decrypt, {error, badarg} =:= GreaterDecResult}
+					])
+			after
+				ok = jose:pbes2_count_maximum(OriginalPBES2CountMaximum)
+			end
+		end).
+
 prop_from_map_and_to_map() ->
 	?FORALL(JWEMap,
 		?LET({{_Key, _JWKMap, JWEMap}, Extras},