Require Export PBFT.


Section PBFTcollision_resistant.

  Local Open Scope eo.
  Local Open Scope proc.

  Context { pbft_context : PBFTcontext      }.
  Context { pbft_auth    : PBFTauth         }.
  Context { pbft_keys    : PBFTinitial_keys }.
  Context { pbft_hash    : PBFThash         }.


  Class PBFThash_axioms :=
    {
      create_hash_messages_collision_resistant :
        forall msgs1 msgs2,
          create_hash_messages msgs1 = create_hash_messages msgs2
          -> msgs1 = msgs2;

      create_hash_state_last_reply_collision_resistant :
        forall sm1 sm2 last1 last2,
          create_hash_state_last_reply sm1 last1 = create_hash_state_last_reply sm2 last2
          -> sm1 = sm2 /\ last1 = last2
    }.

  Context { pbft_hash_axioms : PBFThash_axioms }.

End PBFTcollision_resistant.
