Theory Malicious_Defs

section ‹Malicious Security›

text ‹Here we define security in the malicious security setting. We follow the definitions given in 
\<^cite>‹"DBLP:series/isc/HazayL10"› and \<^cite>‹"DBLP:books/cu/Goldreich2004"›. The definition of malicious security 
follows the real/ideal world paradigm.›

subsection ‹Malicious Security Definitions›

theory Malicious_Defs imports
  CryptHOL.CryptHOL
begin

type_synonym ('in1','aux', 'P1_S1_aux') P1_ideal_adv1 = "'in1' ⇒ 'aux' ⇒ ('in1' × 'P1_S1_aux') spmf"

type_synonym ('in1', 'aux', 'out1', 'P1_S1_aux', 'adv_out1') P1_ideal_adv2 = "'in1' ⇒ 'aux' ⇒ 'out1' ⇒ 'P1_S1_aux' ⇒ 'adv_out1' spmf"

type_synonym ('in1', 'aux', 'out1', 'P1_S1_aux', 'adv_out1') P1_ideal_adv = "('in1','aux', 'P1_S1_aux') P1_ideal_adv1 × ('in1', 'aux', 'out1', 'P1_S1_aux', 'adv_out1') P1_ideal_adv2"

type_synonym ('P1_real_adv', 'in1', 'aux', 'P1_S1_aux') P1_sim1 = "'P1_real_adv' ⇒ 'in1' ⇒ 'aux' ⇒ ('in1' × 'P1_S1_aux') spmf"

type_synonym ('P1_real_adv', 'in1', 'aux', 'out1', 'P1_S1_aux', 'adv_out1') P1_sim2 
                  = "'P1_real_adv' ⇒ 'in1' ⇒ 'aux' ⇒ 'out1' 
                      ⇒ 'P1_S1_aux' ⇒ 'adv_out1' spmf"

type_synonym ('P1_real_adv', 'in1', 'aux', 'out1', 'P1_S1_aux', 'adv_out1') P1_sim  
                = "(('P1_real_adv', 'in1', 'aux', 'P1_S1_aux') P1_sim1 
                    × ('P1_real_adv', 'in1', 'aux', 'out1', 'P1_S1_aux', 'adv_out1') P1_sim2)"

type_synonym ('in2','aux', 'P2_S2_aux') P2_ideal_adv1 = "'in2' ⇒ 'aux' ⇒ ('in2' × 'P2_S2_aux') spmf"

type_synonym ('in2', 'aux', 'out2', 'P2_S2_aux', 'adv_out2') P2_ideal_adv2 
                = "'in2' ⇒ 'aux' ⇒ 'out2' ⇒ 'P2_S2_aux' ⇒ 'adv_out2' spmf"

type_synonym ('in2', 'aux', 'out2', 'P2_S2_aux', 'adv_out2') P2_ideal_adv 
                    = "('in2','aux', 'P2_S2_aux') P2_ideal_adv1 
                        × ('in2', 'aux', 'out2', 'P2_S2_aux', 'adv_out2') P2_ideal_adv2"

type_synonym ('P2_real_adv', 'in2', 'aux', 'P2_S2_aux') P2_sim1 = "'P2_real_adv' ⇒ 'in2' ⇒ 'aux' ⇒ ('in2' × 'P2_S2_aux') spmf"

type_synonym ('P2_real_adv', 'in2', 'aux', 'out2', 'P2_S2_aux', 'adv_out2') P2_sim2 
                  = "'P2_real_adv' ⇒ 'in2' ⇒ 'aux' ⇒ 'out2' 
                      ⇒ 'P2_S2_aux' ⇒ 'adv_out2' spmf"

type_synonym ('P2_real_adv', 'in2', 'aux', 'out2', 'P2_S2_aux', 'adv_out2') P2_sim 
                  = "(('P2_real_adv', 'in2', 'aux', 'P2_S2_aux') P2_sim1 
                      × ('P2_real_adv', 'in2', 'aux', 'out2', 'P2_S2_aux', 'adv_out2') P2_sim2)"

locale malicious_base =
  fixes funct :: "'in1 ⇒ 'in2 ⇒ ('out1 × 'out2) spmf" ― ‹the functionality›
    and protocol :: "'in1 ⇒ 'in2 ⇒ ('out1 × 'out2) spmf" ― ‹outputs the output of each party in the protocol›
    and S1_1 :: "('P1_real_adv, 'in1, 'aux, 'P1_S1_aux) P1_sim1" ― ‹first part of the simulator for party 1›
    and S1_2 :: "('P1_real_adv, 'in1, 'aux, 'out1, 'P1_S1_aux, 'adv_out1) P1_sim2" ― ‹second part of the simulator for party 1›
    and P1_real_view :: "'in1 ⇒ 'in2 ⇒ 'aux ⇒ 'P1_real_adv ⇒ ('adv_out1 × 'out2) spmf" ― ‹real view for party 1, the adversary totally controls party 1›
    and S2_1 :: "('P2_real_adv, 'in2, 'aux, 'P2_S2_aux) P2_sim1" ― ‹first part of the simulator for party 2›
    and S2_2 :: "('P2_real_adv, 'in2, 'aux, 'out2, 'P2_S2_aux, 'adv_out2) P2_sim2" ― ‹second part of the simulator for party 1›
    and P2_real_view :: "'in1 ⇒ 'in2 ⇒ 'aux ⇒ 'P2_real_adv ⇒ ('out1 × 'adv_out2) spmf" ― ‹real view for party 2, the adversary totally controls party 2›
begin

definition "correct m1 m2 ⟷ (protocol m1 m2 = funct m1 m2)"

abbreviation "trusted_party x y ≡ funct x y"

text‹The ideal game defines the ideal world. First we consider the case where party 1 is corrupt, and thus 
controlled by the adversary. The adversary is split into two parts, the first part takes the original input and 
auxillary information and outputs its input to the protocol. The trusted party then computes the functionality on
the input given by the adversary and the correct input for party 2. Party 2 outputs the its correct output as
given by the trusted party, the adversary provides the output for party 1.›

definition ideal_game_1 :: "'in1 ⇒ 'in2 ⇒ 'aux ⇒ ('in1, 'aux, 'out1, 'P1_S1_aux, 'adv_out1) P1_ideal_adv ⇒ ('adv_out1 × 'out2) spmf"
  where "ideal_game_1 x y z A = do {
    let (A1,A2) = A;
    (x', aux_out) ← A1 x z;
    (out1, out2) ← trusted_party x' y; 
    out1' :: 'adv_out1 ← A2 x' z out1 aux_out; 
    return_spmf (out1', out2)}" 

definition ideal_view_1 :: "'in1 ⇒ 'in2 ⇒ 'aux ⇒ ('P1_real_adv, 'in1, 'aux, 'out1, 'P1_S1_aux, 'adv_out1) P1_sim ⇒ 'P1_real_adv ⇒ ('adv_out1 × 'out2) spmf"
  where "ideal_view_1 x y z S 𝒜 = (let (S1, S2) = S in (ideal_game_1 x y z (S1 𝒜, S2 𝒜)))" 

text‹We have information theoretic security when the real and ideal views are equal.›

definition "perfect_sec_P1 x y z S 𝒜 ⟷ (ideal_view_1 x y z S 𝒜 = P1_real_view x y z 𝒜)"

text‹The advantage of party 1 denotes the probability of a distinguisher distinguishing the real and 
ideal views.›

definition "adv_P1 x y z S 𝒜 (D :: ('adv_out1 × 'out2) ⇒ bool spmf) = 
                ¦spmf (P1_real_view x y z 𝒜 ⤜ (λ view. D view)) True
                    - spmf (ideal_view_1 x y z S 𝒜 ⤜ (λ view. D view)) True ¦" 

definition ideal_game_2 :: "'in1 ⇒ 'in2 ⇒ 'aux ⇒ ('in2, 'aux, 'out2, 'P2_S2_aux, 'adv_out2) P2_ideal_adv ⇒ ('out1 × 'adv_out2) spmf"
  where "ideal_game_2 x y z A = do {
    let (A1,A2) = A;
    (y', aux_out) ← A1 y z; 
    (out1, out2) ← trusted_party x y';
    out2' :: 'adv_out2 ← A2 y' z out2 aux_out; 
    return_spmf (out1, out2')}"   

definition ideal_view_2 :: "'in1 ⇒ 'in2 ⇒ 'aux ⇒ ('P2_real_adv, 'in2, 'aux, 'out2, 'P2_S2_aux, 'adv_out2) P2_sim ⇒ 'P2_real_adv ⇒ ('out1 × 'adv_out2) spmf"
  where "ideal_view_2 x y z S 𝒜 = (let (S1, S2) = S in (ideal_game_2 x y z (S1 𝒜, S2 𝒜)))" 

definition "perfect_sec_P2 x y z S 𝒜 ⟷ (ideal_view_2 x y z S 𝒜 = P2_real_view x y z 𝒜)"

definition "adv_P2 x y z S 𝒜 (D :: ('out1 × 'adv_out2) ⇒ bool spmf) = 
                ¦spmf (P2_real_view x y z 𝒜 ⤜ (λ view. D view)) True
                    - spmf (ideal_view_2 x y z S 𝒜 ⤜ (λ view. D view)) True ¦" 


end

end