diff --git a/src/program_proof/pav/crypto_model.v b/src/program_proof/pav/crypto_model.v
index a79296369..abbe7bee2 100644
--- a/src/program_proof/pav/crypto_model.v
+++ b/src/program_proof/pav/crypto_model.v
@@ -1,16 +1,20 @@
-(** This file provides an operational model for:
+(** we provide an operational model (encoded as a labeled transition
+system) for:
 1) an EUF-CMA signature scheme.
 2) a collision-resistant random oracle hash function.
 
-Hopefully, we can prove the admitted iProps in cryptoffi.v from it. *)
+to gain assurance in the model, we prove trace invariants that capture the
+core cryptographic properties of both operations.
+see [sig_correct], [sig_unforg], and [coll_resis].
+
+we should be able to prove the admitted iProps in cryptoffi.v from this. *)
 
-From Coq Require Import ssreflect.
-(* not using the BI parts, just gset_bijective. *)
-From iris.algebra.lib Require Import gset_bij.
-From Perennial.Helpers Require Import Integers.
-From stdpp Require Import prelude gmap.
 From RecordUpdate Require Import RecordSet.
 Import RecordSetNotations.
+From Perennial.Helpers Require Import Integers.
+From stdpp Require Import ssreflect prelude gmap.
+(* not using the BI parts, just gset_bijective. *)
+From iris.algebra.lib Require Import gset_bij.
 
 Section shared.
 
@@ -70,18 +74,7 @@ the other divergence is how we capture the constraint of a poly time adversary.
 the main capability of super-poly adversaries is their ability to run crypto ops
 a huge number of times to exhibit collisions.
 we block this, by having the underlying machine infinite loop exactly when
-it detects a collision.
-
-one way to gain confidence in the model is to show that the traces
-generated by it satisfy some core EUF-CMA trace invariants, such as:
-1) you can't forge sigs.
-  if verify pk m s = true at state i, then exists j ≤ i s.t. at state j, sign sk m = s'.
-2) correctness.
-  if sign sk m = s, not exist state i with verify pk m s = false.
-3) verify is deterministic.
-  if verify pk m s = b1 at state i and verify pk m s = b2 at state j, then b1 = b2.
-a smaller example of such a trace invariant can be found in the hash model
-collision resistance lemma below. *)
+it detects a collision. *)
 Definition step (prev_st : state_ty) (trans : trans_ty) (next_st : state_ty) : Prop :=
   match trans.(op) with
   | key_gen =>
@@ -156,6 +149,56 @@ Definition step (prev_st : state_ty) (trans : trans_ty) (next_st : state_ty) : P
     end
   end.
 
+Record trace_ty :=
+  mk_trace {
+    states: list state_ty;
+    labels: list trans_ty;
+  }.
+
+Definition valid_trace (t : trace_ty) :=
+  (∀ a, t.(states) !! 0 = Some a → a.(key_distr) = ∅ ∧ a.(verify_memo) = ∅) ∧
+  Forall3 (λ a b c, step a b c)
+    (take (pred (length t.(states))) t.(states))
+    t.(labels)
+    (drop 1 t.(states)).
+
+Lemma keys_bij {t i s} :
+  valid_trace t →
+  t.(states) !! i = Some s →
+  gset_bijective s.(key_distr).
+Proof. Admitted.
+
+Lemma sig_correct {t i k st_i sk pk msg sig ok} :
+  valid_trace t →
+  (* valid key. *)
+  t.(states) !! i = Some st_i →
+  set_Exists (λ x, x = (sk, pk)) st_i.(key_distr) →
+  (* called sign. *)
+  t.(labels) !! i = Some (mk_trans (sign sk msg) (ret_sign sig)) →
+  (* called verify. *)
+  t.(labels) !! (i + k) = Some (mk_trans (verify pk msg sig) (ret_verify ok)) →
+  (* verify will return true. *)
+  ok = true.
+Proof. Admitted.
+
+Lemma sig_unforg {t i st_i sk pk msg sig ok} :
+  valid_trace t →
+  (* valid key. *)
+  t.(states) !! i = Some st_i →
+  set_Exists (λ x, x = (sk, pk)) st_i.(key_distr) →
+  (* never signed msg before.
+  modeling with verify_memo would under-approx adv ability,
+  since adv can forge some sigs.
+  this label modeling is more precise. *)
+  (∀ j sig',
+    j < i →
+    t.(labels) !! j ≠ Some (mk_trans (sign sk msg) (ret_sign sig'))) →
+  (* called verify with some sig. *)
+  t.(labels) !! i = Some (mk_trans (verify pk msg sig) (ret_verify ok)) →
+  (* verify will return false. *)
+  ok = false.
+Proof. Admitted.
+
 End signatures.
 
 Module hashes.
@@ -177,7 +220,6 @@ Inductive op_ty : Type :=
 Inductive ret_ty : Type :=
   | ret_hash : hash_ty → ret_ty.
 
-(* transitions. *)
 Record trans_ty :=
   mk_trans {
     op: op_ty;