%%
%% %CopyrightBegin%
%% 
%% Copyright Ericsson AB 2004-2015. All Rights Reserved.
%% 
%% The contents of this file are subject to the Erlang Public License,
%% Version 1.1, (the "License"); you may not use this file except in
%% compliance with the License. You should have received a copy of the
%% Erlang Public License along with this software. If not, it can be
%% retrieved online at http://www.erlang.org/.
%% 
%% Software distributed under the License is distributed on an "AS IS"
%% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See
%% the License for the specific language governing rights and limitations
%% under the License.
%% 
%% %CopyrightEnd%
%%
%%

-module(ssl_eqc_handshake).

-compile(export_all).

-proptest(eqc).
-proptest([triq,proper]).

-ifndef(EQC).
-ifndef(PROPER).
-ifndef(TRIQ).
-define(EQC,true).
-endif.
-endif.
-endif.

-ifdef(EQC).
-include_lib("eqc/include/eqc.hrl").
-define(MOD_eqc,eqc).

-else.
-ifdef(PROPER).
-include_lib("proper/include/proper.hrl").
-define(MOD_eqc,proper).

-else.
-ifdef(TRIQ).
-define(MOD_eqc,triq).
-include_lib("triq/include/triq.hrl").

-endif.
-endif.
-endif.

-include_lib("ssl/src/tls_handshake_1_3.hrl").
-include_lib("ssl/src/tls_handshake.hrl").
-include_lib("ssl/src/ssl_handshake.hrl").
-include_lib("ssl/src/ssl_alert.hrl").
-include_lib("ssl/src/ssl_internal.hrl").

-define('TLS_v1.3', {3,4}).
-define('TLS_v1.2', {3,3}).
-define('TLS_v1.1', {3,2}).
-define('TLS_v1',   {3,1}).
-define('SSL_v3',   {3,0}).

%%--------------------------------------------------------------------
%% Properties --------------------------------------------------------
%%--------------------------------------------------------------------

prop_tls_hs_encode_decode() ->
    ?FORALL({Handshake, TLSVersion}, ?LET(Version, tls_version(), {tls_msg(Version), Version}),
            try 
                [Type, _Length, Data] = tls_handshake:encode_handshake(Handshake, TLSVersion),
                case tls_handshake:decode_handshake(TLSVersion, Type, Data) of
                    Handshake ->
                        true;
                    _ ->
                        false
                end
            catch
                throw:#alert{} ->
                    true
            end
	   ).

tls_version() ->
    oneof([?'TLS_v1.2', ?'TLS_v1.1', ?'TLS_v1', ?'SSL_v3']). 

tls_msg(?'TLS_v1.3'= Version) ->
    oneof([client_hello(Version),
           %%server_hello(Version)
           %%new_session_ticket()
           #end_of_early_data{},
           %%encrypted_extensions()
           %%certificate_1_3(),
           %%certificate_request()
           %%certificate_verify()
           %%finished()
           key_update()
           %%message_hash()
          ]);
tls_msg(Version) ->
    oneof([#hello_request{},
           client_hello(Version),
           %%server_hello(Version)
           %%certificate(),
           %%server_key_exchange()
           %%certificate_request()
           #server_hello_done{}
           %%certificate_verify()
           %%client_key_exchange()
           %%finished()
          ]).

client_hello(?'TLS_v1.3' = Version) ->
    #client_hello{session_id = session_id(),
		  client_version = ?'TLS_v1.2',
		  cipher_suites = ssl_cipher:suites(Version), 
		  compression_methods = compressions(Version),
		  random = client_random(Version),
		  extensions = client_extensions(Version)    
                 };
client_hello(Version) ->
    #client_hello{session_id = session_id(),
		  client_version = Version,
		  cipher_suites = ssl_cipher:suites(Version), 
		  compression_methods = compressions(Version),
		  random = client_random(Version),
		  extensions = client_extensions(Version)    
                 }.
session_id() ->
    crypto:strong_rand_bytes(?NUM_OF_SESSION_ID_BYTES).
 
compressions(_) -> 
    ssl_record:compressions().
client_random(_) ->
    crypto:strong_rand_bytes(32).
       
client_extensions(_) ->
    #hello_extensions{}.

key_update() ->
    #key_update{request_update = request_update()}.

request_update() ->
     oneof([?UPDATE_NOT_REQUESTED, ?UPDATE_REQUESTED]).