Skip to content

Commit

Permalink
Merge branch 'main' into twal/better_label_smtpattern
Browse files Browse the repository at this point in the history
  • Loading branch information
@TWal
TWal authored Oct 17, 2024
2 parents fed53ac + 47c7c65 commit 4d3cdad
Show file tree
Hide file tree
Showing 4 changed files with 11 additions and 29 deletions.
18 changes: 3 additions & 15 deletions src/core/DY.Core.Attacker.Knowledge.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -174,18 +174,6 @@ val attacker_knows: trace -> bytes -> prop
let attacker_knows tr msg =
exists step. attacker_knows_aux step tr msg

val move_requires_4
(#a #b #c #d: Type)
(#p #q: (a -> b -> c -> d -> Type))
($_: (x: a -> y: b -> z: c -> w: d -> Lemma (requires (p x y z w)) (ensures (q x y z w))))
(x: a)
(y: b)
(z: c)
(w: d)
: Lemma (p x y z w ==> q x y z w)
let move_requires_4 #a #b #c #d #p #q pf x y z w =
introduce p x y z w ==> q x y z w with _. pf x y z w

/// Lemma for the base case of the attacker knowledge theorem:
/// bytestrings that the attacker obtained by corruption
/// are publishable.
Expand Down Expand Up @@ -223,8 +211,8 @@ let rec attacker_only_knows_publishable_values_aux #invs step tr msg =
FStar.Classical.forall_intro (FStar.Classical.move_requires (attacker_only_knows_publishable_values_aux (step-1) tr));
FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (concat_preserves_publishability tr));
FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (split_preserves_publishability tr));
FStar.Classical.forall_intro_4 ( move_requires_4 (aead_enc_preserves_publishability tr));
FStar.Classical.forall_intro_4 ( move_requires_4 (aead_dec_preserves_publishability tr));
FStar.Classical.forall_intro_4 (FStar.Classical.move_requires_4 (aead_enc_preserves_publishability tr));
FStar.Classical.forall_intro_4 (FStar.Classical.move_requires_4 (aead_dec_preserves_publishability tr));
FStar.Classical.forall_intro (FStar.Classical.move_requires (pk_preserves_publishability tr));
FStar.Classical.forall_intro_3 (FStar.Classical.move_requires_3 (pk_enc_preserves_publishability tr));
FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (pk_dec_preserves_publishability tr));
Expand All @@ -235,7 +223,7 @@ let rec attacker_only_knows_publishable_values_aux #invs step tr msg =
FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (dh_preserves_publishability tr));
FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (kdf_extract_preserves_publishability tr));
FStar.Classical.forall_intro_3 (FStar.Classical.move_requires_3 (kdf_expand_preserves_publishability tr));
FStar.Classical.forall_intro_4 ( move_requires_4 (kdf_expand_shorter_preserves_publishability tr));
FStar.Classical.forall_intro_4 (FStar.Classical.move_requires_4 (kdf_expand_shorter_preserves_publishability tr));
FStar.Classical.forall_intro (FStar.Classical.move_requires (kem_pk_preserves_publishability tr));
FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (kem_encap_preserves_publishability tr));
FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (kem_decap_preserves_publishability tr));
Expand Down
5 changes: 2 additions & 3 deletions src/lib/state/DY.Lib.State.PKI.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,8 +47,7 @@ instance map_types_pki: map_types pki_key pki_value = {
ps_value_t = ps_pki_value;
}

// The `#_` at the end is a workaround for FStarLang/FStar#3286
val pki_pred: {|crypto_invariants|} -> map_predicate pki_key pki_value #_
val pki_pred: {|crypto_invariants|} -> map_predicate pki_key pki_value
let pki_pred #cinvs = {
pred = (fun tr prin sess_id (key: pki_key) value ->
is_public_key_for tr value.public_key key.ty key.who
Expand All @@ -68,7 +67,7 @@ let pki_tag_and_invariant #ci = (|map_types_pki.tag, local_state_predicate_to_lo

[@@ "opaque_to_smt"]
val initialize_pki: prin:principal -> traceful state_id
let initialize_pki = initialize_map pki_key pki_value #_ // another workaround for FStarLang/FStar#3286
let initialize_pki = initialize_map pki_key pki_value

[@@ "opaque_to_smt"]
val install_public_key: principal -> state_id -> long_term_key_type -> principal -> bytes -> traceful (option unit)
Expand Down
5 changes: 2 additions & 3 deletions src/lib/state/DY.Lib.State.PrivateKeys.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,9 +91,8 @@ let is_public_key_for #cinvs tr pk pk_type who =
is_verification_key (long_term_key_type_to_usage pk_type who) (long_term_key_label who) tr pk
)

// The `#_` at the end is a workaround for FStarLang/FStar#3286
#push-options "--z3rlimit 10"
val private_keys_pred: {|crypto_invariants|} -> map_predicate private_key_key private_key_value #_
val private_keys_pred: {|crypto_invariants|} -> map_predicate private_key_key private_key_value
let private_keys_pred #cinvs = {
pred = (fun tr prin sess_id key value ->
is_private_key_for tr value.private_key key.ty prin
Expand All @@ -114,7 +113,7 @@ let private_keys_tag_and_invariant #ci = (|map_types_private_keys.tag, local_sta

[@@ "opaque_to_smt"]
val initialize_private_keys: prin:principal -> traceful state_id
let initialize_private_keys = initialize_map private_key_key private_key_value #_ // another workaround for FStarLang/FStar#3286
let initialize_private_keys = initialize_map private_key_key private_key_value

[@@ "opaque_to_smt"]
val generate_private_key: principal -> state_id -> long_term_key_type -> traceful (option unit)
Expand Down
12 changes: 4 additions & 8 deletions src/lib/utils/DY.Lib.Printing.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -116,8 +116,7 @@ let long_term_key_type_to_string t =
| DY.Lib.State.PrivateKeys.LongTermPkEncKey u -> "LongTermPkEncKey " ^ u
| DY.Lib.State.PrivateKeys.LongTermSigKey u -> "LongTermSigKey " ^ u

// The `#_` at the end is a workaround for FStarLang/FStar#3286
val private_keys_types_to_string: (list (map_elem DY.Lib.State.PrivateKeys.private_key_key DY.Lib.State.PrivateKeys.private_key_value #_)) -> string
val private_keys_types_to_string: (list (map_elem DY.Lib.State.PrivateKeys.private_key_key DY.Lib.State.PrivateKeys.private_key_value)) -> string
let rec private_keys_types_to_string m =
match m with
| [] -> ""
Expand All @@ -126,8 +125,7 @@ let rec private_keys_types_to_string m =
Printf.sprintf "%s = (%s)," (long_term_key_type_to_string hd.key.ty) (bytes_to_string hd.value.private_key)
)

// The `#_` at the end is a workaround for FStarLang/FStar#3286
val pki_types_to_string: (list (map_elem DY.Lib.State.PKI.pki_key DY.Lib.State.PKI.pki_value #_)) -> string
val pki_types_to_string: (list (map_elem DY.Lib.State.PKI.pki_key DY.Lib.State.PKI.pki_value)) -> string
let rec pki_types_to_string m =
match m with
| [] -> ""
Expand All @@ -138,14 +136,12 @@ let rec pki_types_to_string m =

val default_private_keys_state_to_string: bytes -> option string
let default_private_keys_state_to_string content_bytes =
// another workaround for FStarLang/FStar#3286
let? state = parse (map DY.Lib.State.PrivateKeys.private_key_key DY.Lib.State.PrivateKeys.private_key_value #_) content_bytes in
let? state = parse (map DY.Lib.State.PrivateKeys.private_key_key DY.Lib.State.PrivateKeys.private_key_value) content_bytes in
Some (Printf.sprintf "[%s]" (private_keys_types_to_string state.key_values))

val default_pki_state_to_string: bytes -> option string
let default_pki_state_to_string content_bytes =
// another workaround for FStarLang/FStar#3286
let? state = parse (map DY.Lib.State.PKI.pki_key DY.Lib.State.PKI.pki_value #_) content_bytes in
let? state = parse (map DY.Lib.State.PKI.pki_key DY.Lib.State.PKI.pki_value) content_bytes in
Some (Printf.sprintf "[%s]" (pki_types_to_string state.key_values))

/// Searches for a printer with the correct tag
Expand Down

0 comments on commit 4d3cdad

Please sign in to comment.