← Back

Modules

Leios

  • Abstract
  • Base
  • Blocks
  • Config
  • Defaults
  • FFD
  • Foreign.BaseTypes
  • Foreign.HsTypes
  • Foreign.Types
  • Foreign.Util
  • KeyRegistration
  • Network
  • Prelude
  • Protocol
  • Short
  • Short.Trace.Verifier
  • Simplified
  • Simplified.Deterministic
  • SpecStructure
  • Traces
  • Voting
  • VRF

Network

  • BasicBroadcast
  • Leios
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950
open import Leios.Prelude hiding (_⊗_; module Any)
open import CategoricalCrypto
 
module Network.BasicBroadcast (Participants : ℕ) (Message : Type) where
 
data NetworkT : ChannelDir → Type where
RcvMessage : Message → NetworkT In
Activate : NetworkT In
SndMessage : List Message → NetworkT Out
 
Participant = Fin Participants
 
private variable buffer buffer₁ buffer₂ : List (Message × Participant)
ms : List Message
p : Participant
k : ℕ
m : Message
x : Message × Participant
 
A : Channel
A = simpleChannel (Message × Participant) (ℕ ⊎ ℕ)
 
M : Channel
M = simpleChannel' NetworkT
 
Ms : Channel
Ms = ⨂ const {B = Participant} M
 
data Receive_withState_return_ : MachineType I (Ms ⊗ A) (List (Message × Participant)) where
 
Send : Receive (honestInputI $ snd⨂ p (-, SndMessage ms)) -- p wants to send messages ms
withState buffer
return (concatMap (λ m → tabulate (m ,_)) ms ++ buffer -- buffer a copy of every message for every participant
, just (honestOutputO $ rcv⨂ p (-, Activate))) -- return control to p
 
Deliver : length buffer₁ ≡ k
→ Receive (adversarialInput (-, inj₁ k)) -- adversary wants to deliver k-th message
withState (buffer₁ ++ (m , p) ∷ buffer₂) -- state decomposes appropriately
return (buffer₁ ++ buffer₂ -- remove message
, just (honestOutputO $ rcv⨂ p (-, RcvMessage m))) -- deliver it
 
Eavesdrop : length buffer₁ ≡ k
→ Receive (adversarialInput (-, inj₂ k)) -- adversary wants to know k-th message
withState (buffer₁ ++ x ∷ buffer₂) -- state decomposes appropriately
return (buffer₁ ++ x ∷ buffer₂
, just (adversarialOutput (-, x))) -- deliver it
 
Network : Machine I (Ms ⊗ A)
Network .Machine.State = List (Message × Participant)
Network .Machine.stepRel = Receive_withState_return_