1%%
2%% %CopyrightBegin%
3%%
4%% Copyright Ericsson AB 2004-2020. All Rights Reserved.
5%%
6%% Licensed under the Apache License, Version 2.0 (the "License");
7%% you may not use this file except in compliance with the License.
8%% You may obtain a copy of the License at
9%%
10%%     http://www.apache.org/licenses/LICENSE-2.0
11%%
12%% Unless required by applicable law or agreed to in writing, software
13%% distributed under the License is distributed on an "AS IS" BASIS,
14%% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15%% See the License for the specific language governing permissions and
16%% limitations under the License.
17%%
18%% %CopyrightEnd%
19%%
20%%
21
22-module(crypto_ng_api_stateful).
23
24-compile(export_all).
25
26-include_lib("common_test/include/ct_property_test.hrl").
27-include("crypto_prop_generators.hrl").
28
29%%%================================================================
30%%% Properties:
31
32prop__crypto_init_multi(Config) ->
33    numtests(300,
34             ?FORALL(Cmds, parallel_commands(?MODULE),
35                     begin
36                         RunResult = run_parallel_commands(?MODULE, Cmds),
37                         ct_property_test:present_result(?MODULE, Cmds, RunResult, Config)
38                     end)).
39
40%%%================================================================
41-define(call(F,As), {call,?MODULE,F,As}).
42
43initial_state() ->
44    #{}.
45
46
47command(S) ->
48    frequency(
49      lists:flatten(
50        [
51         {max(0,5-maps:size(S)),
52         ?call(init_crypto, ?LET(Ciph, cipher(),
53                                  [Ciph, key(Ciph), iv(Ciph), block_size(Ciph)]))},
54
55         [{10, ?call(encrypt, [oneof(refs(S)), binary()])
56          }
57          || refs(S) =/= []],
58
59         [{30, ?call(decrypt, ?LET({Refs,{_,[CT|_]}}, oneof(Sc),
60                                   [Refs, CT]))
61          }
62          || Sc <- [[R || {_,{_,Cs}} = R <- maps:to_list(S),
63                          Cs =/= []]
64                   ],
65             Sc =/= [] ],
66[]        ])).
67
68
69precondition(S, {call,?MODULE,decrypt,[Refs,CrT]}) ->
70    %% io:format("precondition(1) ~p Args = ~p, S = ~p", [decrypt,[Refs,CrT],S]),
71    case maps:get(Refs, S) of
72        {_BlockSize,  [CrT|_]} ->
73            %% io:format(" (sym) true~n",[]),
74            true;
75        {_BlockSize,  [CrT|_], _} ->
76            %% io:format(" (dyn) true~n",[]),
77            true;
78        _Other ->
79            %% io:format(" _Other=~p false~n",[_Other]),
80            false
81    end;
82precondition(_S, {call,?MODULE,_Name,_Args}) ->
83    %% io:format("precondition ~p Args = ~p, S = ~p~n", [_Name,_Args,_S]),
84    true.
85
86
87postcondition(_D, _Call, error) ->
88    %% io:format("postcondition ~p:~p error _Call = ~p~n",[?MODULE,?LINE,_Call]),
89    false;
90postcondition(D, {call,?MODULE,decrypt,[Refs,_CrT]}, Result) ->
91    #{Refs := {_BlockSize, _CT, PT}} = D,
92    Size = size(Result),
93    <<Expect:Size/binary, _/binary>> = PT,
94    Expect == Result;
95postcondition(_D, _Call, _Result) ->
96    true.
97
98
99symbolic({var,_}) -> true;
100symbolic(_) -> false.
101
102
103next_state(S, Refs, {call,?MODULE,init_crypto,[_Cipher, _Key, _IV, BlockSize]}=_C) ->
104    case symbolic(Refs) of
105        true ->
106            S#{Refs => {BlockSize, []} };
107        false ->
108            S#{Refs => {BlockSize, [], <<>>} }
109    end;
110
111next_state(S, Res, {call,?MODULE,encrypt,[Refs,Ptxt]}=_C) ->
112%% io:format("next_state enrypt Refs = ~p, S = ~p~n", [Refs,S]),
113    case S of
114        #{Refs := {BlockSize, Cs}} ->
115            S#{Refs := {BlockSize, Cs++[Res]}};
116
117        #{Refs := {BlockSize, Cs,Ps}} ->
118            S#{Refs := {BlockSize, Cs++[Res], <<Ps/binary,Ptxt/binary>>}}
119    end;
120
121next_state(S, Result, {call,?MODULE,decrypt,[Refs,CrT]}=_C) ->
122%% io:format("next_state decrypt Refs = ~p, CrT = ~p, S = ~p~n", [Refs,CrT,S]),
123    case S of
124        #{Refs := {BlockSize, [CrT|Cs]}} ->
125            S#{Refs := {BlockSize, Cs}};
126
127        #{Refs := {BlockSize, [CrT|Cs], Ps0}} ->
128            Sz = size(Result),
129            <<Result:Sz/binary,Ps/binary>> = Ps0,
130            S#{Refs := {BlockSize,Cs,Ps}}
131    end.
132
133%%%================================================================
134-define(ok_error(X),
135        try X of
136            __R -> %% io:format("~p:~p ok! Result = ~p~n", [?MODULE,?LINE,__R]),
137                   __R
138            catch
139                _CC:_EE:_SS ->
140                    io:format("******* ~p:~p  ~p ~p~n~p", [?MODULE,?LINE,_CC,_EE,_SS]),
141                    error
142            end).
143
144init_crypto(Cipher, Key, IV, _BlockSize) ->
145    %% io:format("~p:~p init_crypto~n    (~p,~n     ~p,~n     ~p,~n     ~p)", [?MODULE,?LINE,Cipher,Key,IV,_BlockSize]),
146    ?ok_error({
147                crypto:crypto_init(Cipher, Key, IV, true),
148                crypto:crypto_init(Cipher, Key, IV, false)
149              }).
150
151encrypt({EncRef,_DecRef}, PlainText) ->
152    %% io:format("~p:~p encrypt~n    (~p,~n     ~p) ", [?MODULE,?LINE,EncRef,PlainText]),
153    ?ok_error(crypto:crypto_update(EncRef, PlainText)).
154
155decrypt({_EncRef,DecRef}, CT) ->
156    %% io:format("~p:~p decrypt~n    (~p,~n     ~p)", [?MODULE,?LINE,DecRef,CT]),
157    ?ok_error(crypto:crypto_update(DecRef, CT)).
158
159%%%----------------------------------------------------------------
160refs(S) -> [Refs || {Refs,_} <- maps:to_list(S)].
161
162