==============================================================================
summary of summaries:

analyzed: formal/attest.spthy

  processing time: 0.00s

  sanity_toolchain (exists-trace): verified (2 steps)
  sanity_v01_accept (exists-trace): verified (16 steps)
  sanity_rotate_then_accept (exists-trace): verified (17 steps)
  sanity_mixed_keyset (exists-trace): verified (17 steps)
  sanity_kid_bound_accept (exists-trace): verified (16 steps)
  sanity_retired_key_receipt_still_accepts (exists-trace): verified (16 steps)
  sanity_slot2_issue_and_compromise (exists-trace): verified (12 steps)
  sanity_attacker_distinct_mid (exists-trace): verified (4 steps)
  sanity_same_version_conflict (exists-trace): verified (5 steps)
  sanity_continuity_advance (exists-trace): verified (12 steps)
  sanity_accept_after_advance (exists-trace): verified (27 steps)
  sanity_multihop_advance_compromise (exists-trace): verified (18 steps)
  sanity_hybrid_accept (exists-trace): verified (17 steps)
  reach_rotation_nonactive_signer_flagged (exists-trace): verified (15 steps)
  reach_rotation_same_version_flagged (exists-trace): verified (10 steps)
  reach_rotation_gap_flagged (exists-trace): verified (9 steps)
  reach_compromised_receipt_submitted (exists-trace): verified (16 steps)
  verified_clean_head_honest (all-traces): verified (92 steps)
  rotation_no_hijack (all-traces): verified (11 steps)
  compromised_key_rejected (all-traces): verified (504 steps)
  acceptance_issuer_signed (all-traces): verified (4084 steps)
  old_key_powerless (all-traces): verified (162 steps)
  sanity_revocation_honored (exists-trace): verified (18 steps)
  sanity_none_ignored (exists-trace): verified (18 steps)
  sanity_issued_receipt_revoked (exists-trace): verified (23 steps)
  reach_refund_window_honored (exists-trace): verified (23 steps)
  reach_revocation_out_of_window (exists-trace): verified (19 steps)
  rev_record_authentic (all-traces): verified (2639 steps)
  revocation_auth_soundness (all-traces): verified (2443 steps)
  revocation_effectiveness (all-traces): verified (1381 steps)
  irrevocability_none (all-traces): verified (579 steps)
  refund_window_bound (all-traces): verified (579 steps)
  revoked_view_never_ok (all-traces): verified (2219 steps)
  attack_tofu_revocation_forgery (exists-trace): verified (8 steps)
  pq_receipt_sig_source (all-traces): verified (6 steps)
  no_cross_version_confusion (all-traces): verified (272 steps)
  attack_v01_post_crqc (exists-trace): verified (14 steps)
  attack_tofu_forgery (exists-trace): verified (12 steps)
  attack_mixed_keyset_hijack (exists-trace): verified (18 steps)
  sanity_artifact_manifest_accept (exists-trace): verified (11 steps)
  am_pq_sig_source (all-traces): verified (6 steps)
  no_downgrade_artifact_manifest (all-traces): verified (7 steps)
  sanity_hybrid_revocation_admitted (exists-trace): verified (14 steps)
  rev_pq_sig_source (all-traces): verified (12 steps)
  no_downgrade_revocation_allhybrid (all-traces): verified (2179 steps)

==============================================================================
