Documentation

Cryptlib.Protocols.Pigeonhole.Semantics

Pigeonhole replica and wire-level exchange as labelled transition systems #

States are stores; labels are (request, reply) pairs. The wire-level system rpcLTS is simulated by the abstract replica replicaLTS.

source
def Cryptlib.Protocols.Pigeonhole.Semantics.replicaLTS {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : ℕ) :
Cslib.LTS (Replica.Store Sg) (Replica.Request Sg × Replica.Reply Sg)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance Cryptlib.Protocols.Pigeonhole.Semantics.instDeterministicStoreProdRequestReplyReplicaLTS {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : ℕ) :
    (replicaLTS boxSize).Deterministic
    source
    theorem Cryptlib.Protocols.Pigeonhole.Semantics.replicaLTS_trInv {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : ℕ) :
    (replicaLTS boxSize).TrInv Replica.Valid

    Every step of the replica preserves "every stored box verifies".

    source
    theorem Cryptlib.Protocols.Pigeonhole.Semantics.replicaLTS_reachable_valid {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (boxSize : ℕ) (s : Replica.Store Sg) (h : (replicaLTS boxSize).CanReach Replica.Store.empty s) :
    Replica.Valid s

    Every store reachable from empty is valid.

    source
    def Cryptlib.Protocols.Pigeonhole.Semantics.rpcLTS {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (M : Primitives.MKEM.MKEM.MKEM) (W : Protocol.Wire Sg) (boxSize : ℕ) :
    Cslib.LTS (Replica.Store Sg) (Replica.Request Sg × Replica.Reply Sg)

    The system as a client sees it: each step is one completed rpc exchange.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Cryptlib.Protocols.Pigeonhole.Semantics.rpcLTS_simulated {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (M : Primitives.MKEM.MKEM.MKEM) (W : Protocol.Wire Sg) (boxSize : ℕ) :
      (rpcLTS M W boxSize).IsSimulation (replicaLTS boxSize) fun (s t : Replica.Store Sg) => s = t

      Every wire-level step is a step of the abstract replica.

      source
      theorem Cryptlib.Protocols.Pigeonhole.Semantics.rpcLTS_traces_subset {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (M : Primitives.MKEM.MKEM.MKEM) (W : Protocol.Wire Sg) (boxSize : ℕ) (s : Replica.Store Sg) :
      (rpcLTS M W boxSize).traces s ⊆ (replicaLTS boxSize).traces s

      Every run of the wire-level system is a run of the abstract replica.

      source
      theorem Cryptlib.Protocols.Pigeonhole.Semantics.rpcLTS_trInv {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (M : Primitives.MKEM.MKEM.MKEM) (W : Protocol.Wire Sg) (boxSize : ℕ) :
      (rpcLTS M W boxSize).TrInv Replica.Valid

      Every step over the wire preserves validity.

      source
      theorem Cryptlib.Protocols.Pigeonhole.Semantics.rpcLTS_reachable_valid {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (M : Primitives.MKEM.MKEM.MKEM) (W : Protocol.Wire Sg) (boxSize : ℕ) (s : Replica.Store Sg) (h : (rpcLTS M W boxSize).CanReach Replica.Store.empty s) :
      Replica.Valid s

      Every store reachable over the wire from empty is valid.