Require Import ssreflect ssrbool eqtype ssrnat div.
Require Import Max.
Require Import ZArith_ext Lists_ext String_ext.
Require Import nodup.

Definition max_lst l := fold_left (fun e a => max e a) l O.

Definition Zmax (a b : Z) := if Zle_bool a b then b else a.

Definition Zmax_lst l := fold_left (fun e a => Zmax e a) l 0.

Definition Zmax_lst_opt (l : list Z) (n : option Z) :=
  match n with
    | Some m => Zmax m (Zmax_lst l)
    | None => Zmax (Zmax_lst l) 1
  end.

Local Open Scope zarith_ext_scope.

Module RFC5246.

Definition byte : Type := Z.

Module S41.
Fixpoint bytes2value' (l : list byte) :=
  if l is h :: t then h + bytes2value' t * 2 ^ 8 else 0.
Definition bytes2valueZ (l : list byte) : Z := bytes2value' l.
Definition bytes2valueN (l : list byte) : nat := Zabs_nat (bytes2value' l).
End S41.

Inductive tls_typ : Z -> Z -> Type :=
| opaque : tls_typ 1 1
| arr : forall n, tls_typ n n -> forall m, Zle_bool 0 m -> Zmod m n == 0 -> tls_typ m m
| varr : forall n m (t : tls_typ n m) (k : nat) a b,
  k != O ->
  Zlt_bool b (2 ^^ (k * 8)) -> Zle_bool (2 ^^ ((k - 1) * 8)) b ->
  Zle_bool a b ->
  Zle_bool m ((Z_of_nat k) + b) ->
  tls_typ ((Z_of_nat k) + a) ((Z_of_nat k) + b)
| enum : forall k l n, nodup l ->
  Zlt_bool (Zmax_lst_opt l n) (2 ^^ (k * 8)) ->
  Zle_bool (2 ^^ ((k - 1) * 8)) (Zmax_lst_opt l n) ->
  tls_typ (Z_of_nat k) (Z_of_nat k)
| pair : forall {n1 m1 n2 m2},
  string * tls_typ n1 m1 -> tls_typ n2 m2 -> tls_typ (n1 + n2) (m1 + m2)
| typ_nil : tls_typ 0 0.

Section correct_tls_typ_ind.

Variables (P : forall a b, tls_typ a b -> Prop) (Q : forall a b, string * tls_typ a b -> Prop).
Hypotheses
(H : forall n1 m1 n2 m2 (p : string * tls_typ n1 m1)
          (t : tls_typ n2 m2), Q n1 m1 p -> P n2 m2 t -> P (n1 + n2) (m1 + m2) (pair p t))
(H0 : P 0 0 typ_nil)
(H1 : P 1 1 opaque)
(H2 : forall n (t : tls_typ n n), P n n t ->
  forall m (i : Zle_bool 0 m) (i0 : m mod n == 0),
    P m m (arr n t m i i0))
(H3 : forall n m (t : tls_typ n m), P n m t ->
  forall (k : nat) a b (i : k != 0%N)
    (i0 : Zlt_bool b (2 ^^ (k * 8)))
    (i1 : Zle_bool (2 ^^ ((k - 1) * 8)) b) (i2 : Zle_bool a b)
    (i3 : Zle_bool m (Z_of_nat k + b)),
    P (Z_of_nat k + a) (Z_of_nat k + b) (varr n m t k a b i i0 i1 i2 i3))
(H4 : forall (k : nat) (l : list Z_eqType) n
  (i : nodup l) (i0 : Zlt_bool (Zmax_lst_opt l n) (2 ^^ (k * 8)))
  (i1 : Zle_bool (2 ^^ ((k - 1) * 8)) (Zmax_lst_opt l n)),
  P (Z_of_nat k) (Z_of_nat k) (enum k l n i i0 i1))
(H5 : forall a b t, P a b t -> forall s, Q a b (s, t)).

Fixpoint tls_typ_ind_gen a b t : P a b t :=
  match t as x return P _ _ x with
    | opaque => H1
    | arr n t' m i i0 => H2 n t' (tls_typ_ind_gen _ _ t') m i i0
    | varr n m t' k a b i i0 i1 i2 i3 => H3 n m t' (tls_typ_ind_gen _ _ t') k a b i i0 i1 i2 i3
    | enum k l n i i0 i1 => H4 k l n i i0 i1
    | pair n1 m1 n2 m2 p t' => H n1 m1 n2 m2 p t'
      match p as x return Q n1 m1 x with
         | (p1, p2) => H5 _ _ _ (tls_typ_ind_gen _ _ p2) p1
      end
      (tls_typ_ind_gen _ _ t')
    | typ_nil => H0
  end.

End correct_tls_typ_ind.

Lemma tls_typ_ind_new : forall P : forall a b, tls_typ a b -> Prop,
  P 1 1 opaque ->
  (forall n (t : tls_typ n n), P n n t ->
    forall m (i : Zle_bool 0 m) (i0 : m mod n == 0),
      P m m (arr n t m i i0)) ->
  (forall n m (t : tls_typ n m), P n m t ->
    forall (k : nat) (a b : Z) (i : k != 0%N)
      (i0 : Zlt_bool b (2 ^^ (k * 8)))
      (i1 : Zle_bool (2 ^^ ((k - 1) * 8)) b) (i2 : Zle_bool a b)
      (i3 : Zle_bool m (Z_of_nat k + b)),
      P (Z_of_nat k + a) (Z_of_nat k + b) (varr n m t k a b i i0 i1 i2 i3)) ->
  (forall (k : nat) (l : list Z_eqType) (n : option Z)
    (i : nodup l) (i0 : Zlt_bool (Zmax_lst_opt l n) (2 ^^ (k * 8)))
    (i1 : Zle_bool (2 ^^ ((k - 1) * 8)) (Zmax_lst_opt l n)),
    P (Z_of_nat k) (Z_of_nat k) (enum k l n i i0 i1)) ->
  (forall a b c d s t1 t2, P a b t1 -> P c d t2 -> P _ _ (pair (s, t1) t2)) ->
  P 0 0 typ_nil ->
  forall a b (t : tls_typ a b) , P _ _ t.

Notation "'struct{' a ; .. ; b '}'" := (pair a .. (pair b typ_nil) ..) (at level 10, no associativity,
  format "'[v' 'struct{' a ; .. ; b '}' ']'").
Notation "'struct{}'" := typ_nil.

Fixpoint tls_typ_find_struct_tag {n m} (t : tls_typ n m) (tag:string) : bool :=
match t with
  | pair _ _ _ _ tag' t' => if tag == fst tag' then false else tls_typ_find_struct_tag t' tag
  | _ => true
end.

Fixpoint tls_typ_well_formed {n m} (t : tls_typ n m) : bool :=
match t with
  | opaque => true
  | arr _ t _ _ _ => tls_typ_well_formed t
  | varr _ _ t _ _ _ _ _ _ _ _ => tls_typ_well_formed t
  | enum _ _ _ _ _ _ => true
  | pair _ _ _ _ (tg, rem) tr => tls_typ_well_formed rem && negb (tls_typ_find_struct_tag tr tg) &&
    match tr with
      | pair _ _ _ _ _ _ => tls_typ_well_formed tr
      | typ_nil => true
      | _ => false
    end
  | typ_nil => true
end.

Fixpoint decode n {a b} (t : tls_typ a b) (lst : list byte) : (bool * list byte) :=
  match n with
    | O =>
      match t with
        | opaque => if (1 <= List.length lst)%nat then
                      (true, tail lst)
                    else
                      (false, lst)
        | arr n _ m _ _ => if Zle_bool m (Z_of_nat (List.length lst)) then
                             (true, skipn (Zabs_nat m) lst)
                           else
                             (false, lst)
        | varr n m t' x k a b _ _ _ _ => (false, lst)
        | enum m l _ _ _ _ => if (m <= List.length lst)%nat && (inb Zeq_bool (S41.bytes2valueZ (firstn m lst)) l) then
                                (true, skipn m lst)
                              else
                                (false, lst)
        | pair n1 m1 n2 m2 (tg, t1) t2 => (false, lst)
        | typ_nil => (true, lst)
      end
    | S n' =>
      match t with
        | opaque => if (1 <= List.length lst)%nat then
                      (true, tail lst)
                    else
                      (false, lst)
        | arr n _ m _ _ => if Zle_bool m (Z_of_nat (List.length lst)) then
                             (true, skipn (Zabs_nat m) lst)
                           else
                             (false, lst)
        | varr n m t' k a b _ _ _ _ _ =>
          if (k <= List.length lst)%nat then
            let len := S41.bytes2valueN (rev (firstn k lst)) in
            if (len <= List.length (skipn k lst))%nat then
              let (ret, lst') := fold_left
                (fun a _ => match a with | (acc, buf) =>
                      match buf with
                        | nil => a
                        | _ => if acc then
                                 let (acc', buf') := decode n' t' buf in (acc' && acc, buf')
                               else
                                 (acc, buf)
                      end
                  end)
                (rep tt len)
                (true, firstn len (skipn k lst)) in
              if ret then
                (true, lst' ++ skipn len (skipn k lst))
              else
                (false, lst)
            else
              (false, lst)
          else
            (false, lst)
        | enum m l _ _ _ _ => if (m <= List.length lst)%nat && (inb Zeq_bool (S41.bytes2valueZ (firstn m lst)) l) then
                                (true, skipn m lst)
                              else
                                (false, lst)
        | pair n1 m1 n2 m2 (tg, t1) t2 =>
          let: (a, lst') := decode n' t1 lst in
          let: (a', lst'') := decode n' t2 lst' in
          (a && a', lst'')
        | typ_nil => (true, lst)
      end
  end.

Definition decoder {n m} (t : tls_typ n m) := decode (depth t) t.

Definition decodep {n m} (t : tls_typ n m) lst :=
  let: (acc, lst'):= decoder t lst in acc && (List.length lst' == O).

Fixpoint fixed_length {n m} (t : tls_typ n m) : Z :=
  match t with
    | opaque => 1
    | arr _ _ m _ _ => m
    | varr _ _ _ x _ _ _ _ _ _ _ => Z_of_nat x
    | enum m _ _ _ _ _ => Z_of_nat m
    | pair _ _ _ _ t1 t2 => fixed_length (snd t1) + fixed_length t2
    | str_nil => 0
  end.

Notation "T \[ n \]" := (arr _ T n (refl_equal _) (refl_equal _)) (at level 50).

Notation "T \[[ n \]]" := (arr _ T (Zabs n) (Zle_bool_true _ _ (Zabs_pos _))
  (proj1 (Zeq_is_eq_bool _ _) (Zmod_1_r (Zabs n)))) (at level 50).


Notation "T \< a \.. b \> n " :=
  (varr _ _ T n a b (refl_equal _) (refl_equal _) (refl_equal _) (refl_equal _)
  (refl_equal _))
  (at level 50).

Notation "\enum n \{ lst \}" :=
  (enum n lst None (refl_equal _) (refl_equal _) (refl_equal _)) (at level 50).
Notation "\enum n \{ lst \} m" :=
  (enum n lst (Some m) (refl_equal _) (refl_equal _) (refl_equal _)) (at level 50).

Module S44.
Definition uint8 := opaque.
Definition uint16 := uint8 \[ 2 \].
Definition uint24 := uint8 \[ 3 \].
Definition uint32 := uint8 \[ 4 \].
Definition uint64 := uint8 \[ 8 \].
End S44.

Module S43.
Definition Datum := opaque \[ 3 \].
Definition Data := Datum \[ 9 \].
Definition Data' := opaque \[ 8 \].
Definition Data'' n := opaque \[[ n \]].
Definition mandatory := opaque \< 300 \.. 400 \> 2.
Import S44.
Definition longer := uint16 \< 0 \.. 800 \> 2.
End S43.

Module S45.
Definition red := 3. Definition blue := 5. Definition white := 7.
Definition Color := \enum 1 \{ red :: blue :: white :: nil \}.
Definition sweet := 1. Definition sour := 2. Definition bitter := 4.
Definition Taste := \enum 2 \{ sweet :: sour :: bitter ::nil \} 32000.
End S45.

Record packet (dec : list byte -> bool) : Type := {
  body : list byte ;
  Hcontents : dec body
}.
Implicit Arguments body [dec].
Definition len {dec} (p : packet dec) := List.length (body p).

Definition tls_typ_packet {n m} (T : tls_typ n m) (l : list byte) (Hl : decodep T l) : packet (decodep T).
Defined.

Definition pack2 {dec} (p : packet dec) : {dec : list byte -> bool & packet dec }.
Defined.

Definition unpack2_dec (H : {dec : list byte -> bool & packet dec } ) : list byte -> bool.
Defined.

Definition unpack2 (H : {dec : list byte -> bool & packet dec } ) :
  packet (unpack2_dec H).
Defined.

Definition pack {n m : Z} (T : tls_typ n m) : {n : Z & { m : Z & tls_typ n m } }.
Defined.

Definition unpack_min (H : {n : Z & { m : Z & tls_typ n m } } ) : Z.
Defined.

Definition unpack_max (H : {n : Z & { m : Z & tls_typ n m } } ) : Z.
Defined.

Definition unpack (H : {n : Z & { m : Z & tls_typ n m } } ) :
  tls_typ (unpack_min H) (unpack_max H).
Defined.

Notation "'\{' i ; .. ; j '\}'":= (cons i .. (cons j nil) ..) (at level 70,
  format "'[v' '\{' '//' i ';' '//' .. ';' '//' j '//' '\}' ']'", i at level 71, j at level 71) : select2_scope.
Notation "'selectb(' b '\)' lst" := (select2_m.sel_test (false :: true :: nil) lst (refl_equal _) b) (at level 70,
  format "'[' 'selectb(' b '\)' lst ']' '//'") : select2_scope.
Notation "'select(' z '\:' t '\:' H '\)' lst" := (select2_m.sel_enum z t H lst (refl_equal _) (refl_equal _)) (at level 70,
  format "'[' 'select(' z '\:' t '\:' H '\)' lst ']' '//'") : select2_scope.
Delimit Scope select2_scope with select2.

Module select_m.
Fixpoint sel {A :eqType} (l : list (A * {n : Z & { m : Z & tls_typ n m } })) (z : A) :=
  match l with
    | (hi, ho) :: tl => if hi == z then ho else sel tl z
    | _ => pack typ_nil
  end.

Definition sel_test {A : eqType} (lst : list A) (l : list (A * {n : Z & {m : Z & tls_typ n m} }))
  (_ : forallb (fun x => fst x == snd x) (combine lst (uzip1 l)))
  (z : A) :=
  match lst with
    | nil => pack typ_nil
    | h :: t => if forallb (fun x => fst x == snd x) (combine lst (uzip1 l)) then
                  sel l z
                else
                  pack typ_nil
  end.

Definition sel_enum (z : list byte) {n m} (t : tls_typ n m) (Henum : decodep t z)
  (l : list (Z * {n' : Z & {m' : Z & tls_typ n' m'} }))
  (H : forallb (fun x => fst x == snd x) (combine (lst_enum t) (uzip1 l)))
  (H' : List.length l == List.length (lst_enum t)) :=
  sel_test (lst_enum t) l H (S41.bytes2valueZ z).
End select_m.

Notation "'\{' i ; .. ; j '\}'":= (cons i .. (cons j nil) ..) (at level 70,
  format "'[v' '\{' '//' i ';' '//' .. ';' '//' j '//' '\}' ']'", i at level 71, j at level 71) : select_scope.
Notation "'selectb(' b '\)' lst" := (select_m.sel_test (false :: true :: nil) lst (refl_equal _) b) (at level 70,
  format "'[' 'selectb(' b '\)' lst ']' '//'") : select_scope.
Notation "'select(' z '\:' t '\:' H '\)' lst" := (select_m.sel_enum z t H lst (refl_equal _) (refl_equal _)) (at level 70,
  format "'[' 'select(' z '\:' t '\:' H '\)' lst ']' '//'") : select_scope.
Delimit Scope select_scope with select.


Notation "'\{' i ; .. ; j '\}'":= (cons i .. (cons j nil) ..) (at level 70,
  format "'[v' '\{' '//' i ';' '//' .. ';' '//' j '//' '\}' ']'", i at level 71, j at level 71) : select_decode_scope.
Notation "'selectb(' b '\)' lst" := (select_decode_m.sel_test (false :: true :: nil) lst (refl_equal _) b) (at level 70,
  format "'[' 'selectb(' b '\)' lst ']' '//'") : select_decode_scope.
Notation "'select(' z '\:' t '\:' H '\)' lst" := (select_decode_m.sel_enum z t H lst (refl_equal _)) (at level 70,
  format "'[' 'select(' z '\:' t '\:' H '\)' lst ']' '//'") : select_decode_scope.
Delimit Scope select_decode_scope with select_decode.

Local Open Scope string_scope.

Module S461.
Definition apple := 0. Definition orange := 1. Definition banana := 2.
Definition VariantTag := \enum 1 \{ apple :: orange :: banana :: nil \}.
Definition variable_string_type := opaque \< 0 \.. 10 \> 1.
  Definition fixed_string_type := opaque \[ 10 \].
Import S44.

Definition V1 :=
   struct{ ("number", uint16) ;
           ("string", variable_string_type) }.
Definition V2 :=
   struct{ ("number", uint32) ;
           ("string", fixed_string_type) }.

Definition VariantStructure n (Hn : decodep VariantTag n) := struct{
  ("variant_body", unpack (select(_ \: _ \: Hn \) \{
    (apple, pack V1) ;
    (orange, pack V2) ;
    (banana, pack V2) \}))%select }.

Structure VariantStructure_packet n (Hn : decodep VariantTag n) := {
  variant_body : packet ((select(_ \: _ \: Hn \) \{
    (apple, decodep V1) ;
    (orange, decodep V2) ;
    (banana, decodep V2) \})%select_decode)
}.


End S461.

Module S48.
Import S44.
Definition Example1 :=
  struct{ ("f1", uint8) ;
          ("f2", uint8) }.
End S48.

Module S71.
Definition change_cipher_spec := 1.
Definition type_type := \enum 1 \{ change_cipher_spec :: nil \} 255.
Definition ChangeCipherSpec := struct{
  ("type", type_type)
}.
End S71.

Module S72.
Definition warning := 1. Definition fatal := 2.
Definition AlertLevel := \enum 1 \{ warning :: fatal :: nil \} 255.
Definition close_notify := 0.
Definition unexpected_message := 10.
Definition bad_record_mac := 20.
Definition decryption_failed_RESERVED := 21.
Definition record_overflow := 22.
Definition decompression_failure := 30.
Definition handshake_failure := 40.
Definition no_certificate_RESERVED := 41.
Definition bad_certificate := 42.
Definition unsupported_certificate := 43.
Definition certificate_revoked := 44.
Definition certificate_expired := 45.
Definition certificate_unknown := 46.
Definition illegal_parameter := 47.
Definition unknown_ca := 48.
Definition access_denied := 49.
Definition decode_error := 50.
Definition decrypt_error := 51.
Definition export_restriction_RESERVED := 60.
Definition protocol_version := 70.
Definition insufficient_security := 71.
Definition internal_error := 80.
Definition user_canceled := 90.
Definition no_renogociation := 100.
Definition unsupported_extension := 110.
Definition AlertDescription := \enum 1 \{
close_notify :: unexpected_message :: bad_record_mac :: decryption_failed_RESERVED ::
record_overflow :: decompression_failure :: handshake_failure :: no_certificate_RESERVED ::
bad_certificate :: unsupported_certificate :: certificate_revoked :: certificate_expired ::
certificate_unknown :: illegal_parameter :: unknown_ca :: access_denied :: decode_error ::
decrypt_error :: export_restriction_RESERVED :: protocol_version :: insufficient_security ::
internal_error :: user_canceled :: no_renogociation :: unsupported_extension :: nil\} 255.
Definition Alert :=
   struct{ ("level", AlertLevel) ;
           ("description", AlertDescription) }.
End S72.

Module S74141.
Definition none := 0. Definition md5 := 1. Definition sha1 := 2.
Definition sha224 := 3. Definition sha256 := 4. Definition sha384 := 5.
Definition sha512 := 6.
Definition HashAlgorithm := \enum 1
  \{ none :: md5 :: sha1 :: sha224 :: sha256 :: sha384 :: sha512 :: nil \} 255.
Definition anonymous := 0. Definition rsa := 1.
Definition dsa := 2. Definition ecdsa := 3.
Definition SignatureAlgorithm := \enum 1
  \{ anonymous :: rsa :: dsa :: ecdsa :: nil \} 255.
Definition SignatureAndHashAlgorithm :=
   struct{ ("hash", HashAlgorithm) ;
           ("signature", SignatureAlgorithm) }.
Definition supported_signature_algorithms :=
  SignatureAndHashAlgorithm \< 2 \.. (2 ^ 16 - 2) \> 2.
End S74141.

Module S47.
Import S74141.
Definition DigitallySigned :=
   struct{ ("algorithm", SignatureAndHashAlgorithm) ;
           ("signature", opaque \< 2 \.. (2 ^ 16 - 1) \> 2) }.
End S47.

Module S61.
Definition server := 0. Definition client := 1.
Definition ConnectionEnd := \enum 1 \{ server :: client :: nil \}.
Definition tls_prf_sha256 := 0.
Definition PRFAlgorithm := \enum 1 \{ tls_prf_sha256 :: nil \}.
Definition null_bca := 0.
Definition rc4 := 1. Definition threedes := 2. Definition aes := 3.
Definition BulkCipherAlgorithm := \enum 1 \{ null_bca :: rc4 :: threedes :: aes :: nil \}.
Definition stream := 0. Definition block := 1. Definition aead := 2.
Definition CipherType := \enum 1 \{ stream :: block :: aead :: nil \}.
Definition null_ma := 0.
Definition hmac_md5 := 1. Definition hmac_sha1 := 2. Definition hmac_sha256 := 3.
Definition hmac_sha384 := 4. Definition hmac_sha512 := 5.
Definition MACAlgorithm := \enum 1 \{ null_ma :: hmac_md5 :: hmac_sha1 :: hmac_sha256 ::
  hmac_sha384 :: hmac_sha512 :: nil \}.
Definition null := 0.
Definition CompressionMethod := \enum 1 \{ null :: nil \} 255.
Import S44.
Definition SecurityParameters :=
  struct{ ("entity", ConnectionEnd) ;
          ("prf_algorithm", PRFAlgorithm) ;
          ("bulk_cipher_algorithm", BulkCipherAlgorithm) ;
          ("cipher_type", CipherType) ;
          ("enc_key_length", uint8) ;
          ("block_length", uint8) ;
          ("fixed_iv_length", uint8) ;
          ("record_iv_length", uint8) ;
          ("mac_algorithm", MACAlgorithm) ;
          ("mac_length", uint8) ;
          ("mak_key_length", uint8) ;
          ("compression_algorithm", CompressionMethod) ;
          ("master_secret", opaque \[ 48 \]) ;
          ("client_random", opaque \[ 32 \]) ;
          ("server_random", opaque \[ 32 \]) }.
End S61.

Module S621.
Import S44.
Definition ProtocolVersion :=
  struct{ ("major", uint8) ;
          ("minor", uint8) }.
Definition change_cipher_spec := 20.
Definition alert := 21.
Definition handshake := 22.
Definition application_data := 23.
Definition ContentType := \enum 1 \{ change_cipher_spec :: alert :: handshake :: application_data :: nil \} 255.

Definition length_maxp (x : list byte) := (S41.bytes2valueN x <= 2 ^ 14)%nat.
Structure TLSPlainText := {
  type : packet (decodep ContentType) ;
  version : packet (decodep ProtocolVersion) ;
  length : packet (fun x => decodep uint16 x && length_maxp x) ;
  fragment : packet (decodep (opaque \[[ S41.bytes2valueZ (body length) \]]))
}.

Definition SSLv30_maj := 3.
Definition SSLv30_min := 0.
Definition TLSv10_maj := SSLv30_maj.
Definition TLSv10_min := 1.
Definition TLSv11_maj := SSLv30_maj.
Definition TLSv11_min := 2.
Definition TLSv12_maj := SSLv30_maj.
Definition TLSv12_min := 3.
Definition TLSPlainText_hd :=
  fixed_length ProtocolVersion + fixed_length ContentType + fixed_length uint16.

End S621.

Module S622.
Import S621 S44.

Definition length_max := (2 ^ 14 + 1024)%nat.
Structure TLSCompressed_packet := {
  type : packet (decodep ContentType) ;
  length : packet (fun x => decodep uint16 x && (S41.bytes2valueN x <= length_max)%nat) ;
  fragment : packet (decodep (opaque \[[ (S41.bytes2valueZ (body length)) \]]))
}.
End S622.

Module S6231.
Definition GenericStreamCipher TLSCompressed_length mac_length :=
   struct{ ("content", opaque \[[ TLSCompressed_length \]]) ;
           ("MAC", opaque \[[ mac_length \]]) }.
End S6231.

Module S6232.
Import S44.
Definition GenericBlockCipher record_iv_length TLSCompressed_length mac_length padding_length :=
  struct{ ("IV", opaque \[[ record_iv_length \]]) ;
          ("blockciphered", struct{ ("content", opaque \[[ TLSCompressed_length \]]) ;
                                    ("MAC", opaque \[[ mac_length \]]) ;
                                    ("padding", uint8 \[[ padding_length \]]) ;
                                    ("padding_length", uint8) }) }.
End S6232.

Module S6233.
Definition GenericAEADCipher record_iv_length TLSCompressed_length :=
   struct{ ("nonce_explicit", opaque \[[ record_iv_length \]]) ;
           ("aead-ciphered", struct{ ("content", opaque \[[ TLSCompressed_length \]]) } ) }.
End S6233.

SearchAbout existT.

Module S623.
Import S621 S44 S61 S6231 S6232 S6233.
Structure TLSCipherText_packet n (Hn : decodep CipherType n) TLSCompressed_length mac_length record_iv_length padding_length := {
  type : packet (decodep ContentType) ;
  version : packet (decodep ProtocolVersion) ;
  length : packet (decodep uint16) ;
  fragment : packet ( (select( _ \: _ \: Hn \) \{
        (stream, decodep (GenericStreamCipher TLSCompressed_length mac_length)) ;
        (block, decodep (GenericBlockCipher record_iv_length TLSCompressed_length mac_length padding_length)) ;
        (aead, decodep (GenericAEADCipher record_iv_length TLSCompressed_length))
      \})%select_decode)
}.
End S623.

Module S7411.
Definition HelloRequest := struct{}.
Definition HelloRequestp := decodep HelloRequest.
Definition HelloRequest_packet := packet HelloRequestp.
End S7411.

Module S7414.
Definition signature_algorithm := 13.
Definition ExtensionType := \enum 2 \{ signature_algorithm :: nil \} 65535.

Definition extension_data_type := opaque \< 0 \.. (2^16 - 1) \> 2.

Definition extension_data_type := opaque \< 0 \.. (2^16 - 1 - 2) \> 2.
Definition Extension :=
  struct{ ("extension_type", ExtensionType) ;
          ("extension_data", extension_data_type) }.
End S7414.

Module S7412.
Import S44.
Definition Random :=
  struct{ ("gmt_unix_time", uint32) ;
          ("random_bytes", opaque \[28\])}.
Definition SessionID := opaque \< 0 \.. 32 \> 1.
Definition CipherSuite := uint8 \[ 2 \].

Definition cipher_suites_type := CipherSuite \< 2 \.. (2^16 - 2) \> 2.
Import S61.
Definition compression_methods_type := CompressionMethod \< 1 \.. (2 ^ 8 - 1) \> 1.
Import S7414.
Definition extensions_type := Extension \< 0 \.. (2^16 - 1) \> 2.
Eval compute in (fixed_length SessionID +
  fixed_length cipher_suites_type +
  fixed_length compression_methods_type).
Import S621.
Eval compute in (fixed_length ProtocolVersion).
Eval compute in (fixed_length Random).
Definition Hello_size (sid : nat) :=
  fixed_length ProtocolVersion + fixed_length Random + fixed_length SessionID + Z_of_nat sid.
Definition ClientHello_size (sid cys cpm : nat) :=
  Hello_size sid +
  fixed_length cipher_suites_type +
  Z_of_nat cys +
  fixed_length compression_methods_type +
  Z_of_nat cpm.
Definition client_extensions_present n (sid cys cpm : nat) :=
  Zlt_bool (ClientHello_size sid cys cpm) (Z_of_nat n).

Structure ClientHello_packet {n} (Hn : decodep uint24 n) := {
  client_version : packet (decodep ProtocolVersion);
  random : packet (decodep Random) ;
  session_id : packet (decodep SessionID) ;
  cipher_suites : packet (decodep cipher_suites_type) ;
  compression_methods : packet (decodep compression_methods_type) ;
  extensions : packet ( (selectb( client_extensions_present (S41.bytes2valueN n)
                (len session_id) (len cipher_suites)
                (len compression_methods) \) \{
        (false, decodep struct{}) ;
        (true, decodep extensions_type) \})%select_decode)
}.
Implicit Arguments client_version [n Hn].
Implicit Arguments random [n Hn].
Implicit Arguments session_id [n Hn].
Implicit Arguments cipher_suites [n Hn].
Implicit Arguments compression_methods [n Hn].
Implicit Arguments extensions [n Hn].

Definition ClientHellop_decoder {n} (Hn : decodep uint24 n) (l : list byte) : bool * list byte :=
let (a', l') := decoder ProtocolVersion l in
let (a'', l'') := decoder Random l' in
let (a3, l3) := decoder SessionID l'' in
let (a4, l4) := decoder cipher_suites_type l3 in
let (a5, l5) := decoder compression_methods_type l4 in
if client_extensions_present (S41.bytes2valueN n)
                (List.length l'' - List.length l3) (List.length l3 - List.length l4)
                (List.length l4 - List.length l5) then
  let (a6, l6) := decoder extensions_type l5 in
  ([&& a', a'', a3, a4, a5 & a6], l6)
else
  ([&& a', a'', a3, a4 & a5], l5).

Definition ClientHellop {n} (Hn : decodep uint24 n) (l : list byte) : bool :=
  let (a, l') := ClientHellop_decoder Hn l in
  (a && (List.length l' == O)).

Lemma ClientHello_packet_ClientHellop : forall n (Hn : decodep uint24 n) (buf : ClientHello_packet Hn),
  ClientHellop Hn
  (body (client_version buf) ++ body (random buf) ++ body (session_id buf) ++
  body (cipher_suites buf) ++ body (compression_methods buf) ++ body (extensions buf)).

End S7412.

Module S7413.
Import S621 S7412 S61 S44.
Definition ServerHello_size (sid : nat) :=
  Hello_size sid + fixed_length CipherSuite + fixed_length CompressionMethod.
Definition server_extensions_present n (fld1 : nat) :=
  Zlt_bool (ServerHello_size fld1) (Z_of_nat n).
Structure ServerHello_packet {n} (Hn : decodep uint24 n) := {
  server_version : packet (decodep ProtocolVersion) ;
  random : packet (decodep Random) ;
  session_id : packet (decodep SessionID) ;
  cipher_suite : packet (decodep CipherSuite) ;
  compression_method : packet (decodep CompressionMethod) ;
  extensions : packet ( (selectb( (server_extensions_present (S41.bytes2valueN n) (len session_id)) \) \{
        (false, decodep struct{} ) ;
        (true, decodep extensions_type)
      \})%select_decode)
}.
Axiom ServerHellop : forall {n}, decodep uint24 n -> list byte -> bool.
End S7413.

Module S742.
Definition ASN1Cert := opaque \< 1 \.. 2^24 - 1 \> 3.
Definition certificate_list_type := ASN1Cert \< 0 \.. 2^24 - 1 \> 3.
Definition Certificate := struct{
  ("certificate_list", certificate_list_type)
}.
Definition Certificatep := decodep Certificate.
End S742.

Module S743.
Definition dhe_dss := 0. Definition dhe_rsa := 1. Definition dh_anon := 2.
Definition rsa := 3. Definition dh_dss := 4. Definition dh_rsa := 5.
Definition KeyExchangeAlgorithm := \enum 1 \{ dhe_dss :: dhe_rsa :: dh_anon ::
  rsa :: dh_dss :: dh_rsa :: nil \}.
Definition dh_p_type := opaque \< 1 \.. 2^16 - 1 \> 2.
Definition dh_g_type := opaque \< 1 \.. 2^16 - 1 \> 2.
Definition dh_Ys := opaque \< 1 \.. 2^16 - 1 \> 2.
Definition ServerDHParams :=
   struct{ ("dh_p", dh_p_type) ;
           ("dh_g", dh_g_type) ;
           ("dh_Ys", dh_Ys) }.
Definition dhe_dss_rsa_type := struct{
  ("params", ServerDHParams) ;
  ("signed_params", struct{
    ("client_random", opaque \[ 32 \]) ;
    ("server_random", opaque \[ 32 \]) ;
    ("params", ServerDHParams)
  }) }.
Definition ServerKeyExchange {n} (Hn : decodep KeyExchangeAlgorithm n) := struct{
  ("params", unpack (select( _ \: _ \: Hn\) \{
    (dhe_dss, pack dhe_dss_rsa_type) ;
    (dhe_rsa, pack dhe_dss_rsa_type) ;
    (dh_anon, pack ServerDHParams) ;
    (rsa, pack struct{}) ;
    (dh_dss, pack struct{}) ;
    (dh_rsa, pack struct{})
  \})%select)
}.
Definition ServerKeyExchangep {n} (Hn : decodep KeyExchangeAlgorithm n) :=
  decodep (ServerKeyExchange Hn).
End S743.

Module S744.
Import S74141.
Definition DistinguishedName := opaque \< 1 \.. 2^16 - 1 \> 2.
Definition rsa_sign := 1. Definition dss_sign := 2. Definition rsa_fixed_dh := 3.
Definition dss_fixed_dh := 4. Definition rsa_ephemeral_dh_RESERVED := 5.
Definition dss_ephemeral_dh_RESERVED := 6. Definition fortezza_dms_RESERVED := 20.
Definition ClientCertificateType := \enum 1 \{ rsa_sign :: dss_sign :: rsa_fixed_dh ::
  dss_fixed_dh :: rsa_ephemeral_dh_RESERVED :: dss_ephemeral_dh_RESERVED ::
  fortezza_dms_RESERVED :: nil \} 255.
Definition CertificateRequest := struct{
  ("certificate_types", ClientCertificateType \< 1 \.. 2^8 - 1 \> 1) ;
  ("supported_signature_algorithms", SignatureAndHashAlgorithm \< 0 \.. 2^16 - 1 \> 2) ;
  ("certificate_authorities", DistinguishedName \< 0 \.. 2^16 - 1 \> 2)
}.
Definition CertificateRequestp := decodep CertificateRequest.
End S744.

Module S745.
Definition ServerHelloDone := struct{}.
Definition ServerHelloDonep := decodep ServerHelloDone.
End S745.

Module S7471.
Import S621.
Definition PreMasterSecret := struct{
  ("client_version", ProtocolVersion) ;
  ("random", opaque \[ 46 \]) }.
Definition EncryptedPreMasterSecret := struct{
  ("pre_master_secret", PreMasterSecret) }.
End S7471.

Module S7472.
Definition implicit := 0. Definition explicit := 1.
Definition PublicValueEncoding := \enum 1 \{ implicit :: explicit :: nil \}.
Definition ClientDiffieHellmanPublic {n} (Hn : decodep PublicValueEncoding n) := struct{
  ("dh_public", unpack (select( _ \: _ \: Hn \) \{
    (implicit, pack struct{}) ;
    (explicit, pack (opaque \< 1 \.. 2^16 - 1\> 2))
    \})%select)
  }.
End S7472.

Module S747.
Import S743 S7471 S7472.
Definition ClientKeyExchange {n} (Hn : decodep KeyExchangeAlgorithm n) {m} (Hm : decodep PublicValueEncoding m) :=
struct{
  ("exchange_keys", unpack (select( _ \: _ \: Hn\) \{
    (dhe_dss, pack (ClientDiffieHellmanPublic Hm)) ;
    (dhe_rsa, pack (ClientDiffieHellmanPublic Hm)) ;
    (dh_anon, pack (ClientDiffieHellmanPublic Hm)) ;
    (rsa, pack EncryptedPreMasterSecret) ;
    (dh_dss, pack (ClientDiffieHellmanPublic Hm)) ;
    (dh_rsa, pack (ClientDiffieHellmanPublic Hm))
  \})%select)
}.
Definition ClientKeyExchangep {n} (Hn : decodep KeyExchangeAlgorithm n) {m} (Hm : decodep PublicValueEncoding m) :=
  decodep (ClientKeyExchange Hn Hm).
End S747.

Module S748.
Definition CertificateVerify (handshake_messages_length : Z) := struct{
  ("handshake_messages", opaque \[[ handshake_messages_length \]])
}.
Definition CertificateVerifyp (handshake_messages_length : Z) :=
  decodep (CertificateVerify handshake_messages_length).
End S748.

Module S749.
Definition verify_data_lengthp x := 12 <= x.
Definition verify_data_type (verify_data_length : Z) :=
  opaque \[[ verify_data_length \]].
Definition Finished (verify_data_length : Z) := struct{ ("verify_data", verify_data_type verify_data_length) }.
Definition Finishedp (verify_data_length : Z) := decodep (Finished verify_data_length).
Definition Finished_packet (x : Z) := packet (Finishedp x).
End S749.

Module S74.
Definition hello_request := 0.
Definition client_hello := 1.
Definition server_hello := 2.
Definition certificate := 11.
Definition server_key_exchange := 12.
Definition certificate_request := 13.
Definition server_hello_done := 14.
Definition certificate_verify := 15.
Definition client_key_exchange := 16.
Definition finished := 20.
Definition HandshakeType := \enum 1 \{ hello_request :: client_hello ::
  server_hello :: certificate :: server_key_exchange :: certificate_request ::
  server_hello_done :: certificate_verify :: client_key_exchange ::
  finished :: nil \} 255.
Import S44 S7411 S7412 S7413 S742 S743 S744 S745 S747 S748 S749 S7472.

Structure Handshake_packet {n} (Hn : decodep KeyExchangeAlgorithm n) {m} (Hm : decodep PublicValueEncoding m)
  (verify_data_length handshake_messages_length : Z) := {
  msg_type : packet (decodep HandshakeType) ;
  length : packet (decodep uint24) ;
  body : packet (fun x => (select( _ \: _ \: Hcontents _ msg_type \) \{
        (hello_request, HelloRequestp) ;
        (client_hello, ClientHellop (Hcontents _ length)) ;
        (server_hello, ServerHellop (Hcontents _ length)) ;
        (certificate, Certificatep) ;
        (server_key_exchange, ServerKeyExchangep Hn) ;
        (certificate_request, CertificateRequestp) ;
        (server_hello_done, ServerHelloDonep) ;
        (certificate_verify, CertificateVerifyp handshake_messages_length) ;
        (client_key_exchange, ClientKeyExchangep Hn Hm) ;
        (finished, Finishedp handshake_messages_length)
      \})%select_decode x && (List.length x == S41.bytes2valueN n))
}.

Definition Handshake_hd := fixed_length HandshakeType + fixed_length uint24.
End S74.

End RFC5246.