Pigeonhole client-replica exchange

A client MKEM-encrypts a request to the replicas; the courier hands each replica its own share; the replica handles the request and seals its reply under the envelope's ephemeral key. Delivery is assumed reliable; courier and replicas honest.

structure Cryptlib.Protocols.Pigeonhole.Protocol.Wire (Sg : Primitives.Sign.Sign.Signature) : Type

Request and reply codecs; decoding undoes encoding.

• reqEnc : Replica.Request Sg → ByteArray
• reqDec : ByteArray → Option (Replica.Request Sg)
• replyEnc : Replica.Reply Sg → ByteArray
• replyDec : ByteArray → Option (Replica.Reply Sg)
• reqDec_reqEnc (r : Replica.Request Sg) : self.reqDec (self.reqEnc r) = some r
• replyDec_replyEnc (r : Replica.Reply Sg) : self.replyDec (self.replyEnc r) = some r

inductive Cryptlib.Protocols.Pigeonhole.Protocol.RpcError : Type

Why an exchange did not complete.

• mkem (e : Primitives.MKEM.MKEM.MKEMError) : RpcError
• badRequest : RpcError
• badReply : RpcError

def Cryptlib.Protocols.Pigeonhole.Protocol.rpc {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (M : Primitives.MKEM.MKEM.MKEM) (W : Wire Sg) (boxSize : ℕ) (cs rs : M.State) (pubs : List { pk : M.PublicKey // M.Safe pk }) (i : ℕ) (skj : M.PrivateKey) (store : Replica.Store Sg) (req : Replica.Request Sg) : Except RpcError (Replica.Store Sg × Replica.Reply Sg)

One exchange with replica i, holding skj. cs, rs are client and replica randomness. Returns the replica's new store and the reply the client sees.

Equations

• One or more equations did not get rendered due to their size.

theorem Cryptlib.Protocols.Pigeonhole.Protocol.rpc_sound {Sg : Primitives.Sign.Sign.Signature} [DecidableEq Sg.PublicKey] (M : Primitives.MKEM.MKEM.MKEM) (W : Wire Sg) (boxSize : ℕ) (cs rs : M.State) (pubs : List { pk : M.PublicKey // M.Safe pk }) (i : ℕ) (hi : i < pubs.length) (skj : M.PrivateKey) (hsk : pubs[i] = ⟨M.derivePublicKey skj, ⋯⟩) (store : Replica.Store Sg) (req : Replica.Request Sg) (r : Replica.Store Sg × Replica.Reply Sg) (h : rpc M W boxSize cs rs pubs i skj store req = Except.ok r) : r = Replica.step boxSize store req

If the exchange completes, the client gets exactly what the replica computed.

Writing a message and reading it back

theorem Cryptlib.Protocols.Pigeonhole.Protocol.write_then_read (M : Primitives.MKEM.MKEM.MKEM) (B : BACAP.Protocol.BACAPSpec) [DecidableEq B.blindable.base.PublicKey] (W : Wire B.blindable.base) (boxSize : ℕ) (sk : B.blindable.base.PrivateKey) (pk : B.blindable.base.PublicKey) (hpk : pk = B.blindable.base.pub sk) (idx : BACAP.Types.MessageBoxIndex) (ctx pt : ByteArray) (store : Replica.Store B.blindable.base) (hfree : store (B.deriveBoxID pk idx ctx) = none) (hne : (B.encryptBox sk pk idx ctx pt).2.1.size ≠ 0) (hsize : (B.encryptBox sk pk idx ctx pt).2.1.size = boxSize) (cs₁ rs₁ cs₂ rs₂ : M.State) (pubs : List { pk : M.PublicKey // M.Safe pk }) (i : ℕ) (hi : i < pubs.length) (skj : M.PrivateKey) (hsk : pubs[i] = ⟨M.derivePublicKey skj, ⋯⟩) : (∀ (r : Replica.Store B.blindable.base × Replica.Reply B.blindable.base), rpc M W boxSize cs₁ rs₁ pubs i skj store (Replica.Request.write (B.encryptBox sk pk idx ctx pt).1 (B.encryptBox sk pk idx ctx pt).2.1 (B.encryptBox sk pk idx ctx pt).2.2) = Except.ok r → r = (store.put (B.encryptBox sk pk idx ctx pt).1 { payload := (B.encryptBox sk pk idx ctx pt).2.1, sig := (B.encryptBox sk pk idx ctx pt).2.2 }, Replica.Reply.writeReply Replica.Code.success)) ∧ (∀ (r : Replica.Store B.blindable.base × Replica.Reply B.blindable.base), rpc M W boxSize cs₂ rs₂ pubs i skj (store.put (B.encryptBox sk pk idx ctx pt).1 { payload := (B.encryptBox sk pk idx ctx pt).2.1, sig := (B.encryptBox sk pk idx ctx pt).2.2 }) (Replica.Request.read (B.deriveBoxID pk idx ctx)) = Except.ok r → r = (store.put (B.encryptBox sk pk idx ctx pt).1 { payload := (B.encryptBox sk pk idx ctx pt).2.1, sig := (B.encryptBox sk pk idx ctx pt).2.2 }, Replica.Reply.readReply Replica.Code.success (some { payload := (B.encryptBox sk pk idx ctx pt).2.1, sig := (B.encryptBox sk pk idx ctx pt).2.2 }))) ∧ B.decryptBox (B.deriveBoxID pk idx ctx) idx ctx (B.encryptBox sk pk idx ctx pt).2.1 (B.encryptBox sk pk idx ctx pt).2.2 = some pt

A message the writer encrypts and writes to a free box is read back by a reader holding only pk, idx and ctx: the write succeeds, the read returns the written box, and it decrypts to pt.