diff --git a/definitions/package.yaml b/definitions/package.yaml
index 17be97b54a..cc02f9f520 100644
--- a/definitions/package.yaml
+++ b/definitions/package.yaml
@@ -29,9 +29,11 @@ dependencies:
   # - polysemy-plugin
   - lens
   - mtl
+  - protocol
   - singletons
   - servant-docs
   - servant-server
+  - text
   - transformers
 
 library:
diff --git a/definitions/src/Control/Protocol.hs b/definitions/src/Control/Protocol.hs
deleted file mode 100644
index d93db6861f..0000000000
--- a/definitions/src/Control/Protocol.hs
+++ /dev/null
@@ -1,78 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
-
-module Control.Protocol
-  ( Protocol,
-    ProtocolCmd,
-    Command,
-    (->:),
-    runProtocol,
-  )
-where
-
-import Control.XFreer
-import Data.Kind
-import Data.Singletons
-import GHC.TypeLits (ErrorMessage (..), TypeError)
-
-type Command party state = (party, state, state) -> (party, state, state) -> Type -> Type
-
-data ProtocolCmd (cmd :: Command p k) (parties :: [p]) (s :: [k]) (s' :: [k]) (a :: Type) where
-  ProtocolCmd ::
-    Sing (from :: p) ->
-    Sing (to :: p) ->
-    cmd '(from, Prj ps s from, fs') '(to, Prj ps s to, ts') a ->
-    ProtocolCmd cmd ps s (Inj ps (Inj ps s from fs') to ts') a
-
-type Protocol cmd parties = XFree (ProtocolCmd cmd parties)
-
-infix 6 ->:
-
-(->:) ::
-  Sing from ->
-  Sing to ->
-  cmd '(from, Prj ps s from, fs') '(to, Prj ps s to, ts') a ->
-  Protocol cmd ps s (Inj ps (Inj ps s from fs') to ts') a
-(->:) f t c = xfree $ ProtocolCmd f t c
-
-runProtocol ::
-  forall m cmd ps s s' a.
-  Monad m =>
-  (forall from to b. (Sing (P from) -> Sing (P to) -> cmd from to b -> m b)) ->
-  Protocol cmd ps s s' a ->
-  m a
-runProtocol runCmd = loop
-  where
-    loop :: forall s1 s2 b. Protocol cmd ps s1 s2 b -> m b
-    loop (Pure x) = return x
-    loop (Bind c f) = run c >>= loop . f
-    run :: forall s1 s2 b. ProtocolCmd cmd ps s1 s2 b -> m b
-    run (ProtocolCmd from to cmd) = runCmd from to cmd
-
-type family P (partyCmd :: (party, s, s)) where
-  P '(p, _, _) = p
-
--- extracts the state of one party from the list of states
-type family Prj (parties :: [pk]) (state :: [k]) (party :: pk) :: k where
-  Prj (p ': _) (s ': _) p = s
-  Prj (_ ': ps) (_ ': ss) p = Prj ps ss p
-  Prj '[] _ p = TypeError (NoParty p)
-  Prj _ '[] p = TypeError (NoParty p :$$: StateError)
-
--- updates the state of some party in the list of states
-type family Inj (parties :: [pk]) (state :: [k]) (p :: pk) (s' :: k) :: [k] where
-  Inj (p ': _) (_ ': ss) p s' = s' ': ss
-  Inj (_ ': ps) (s ': ss) p s' = s ': Inj ps ss p s'
-  Inj '[] _ p _ = TypeError (NoParty p)
-  Inj _ '[] p _ = TypeError (NoParty p :$$: StateError)
-
-type NoParty p = Text "Party " :<>: ShowType p :<>: Text " is not found."
-
-type StateError = Text "Specified fewer protocol states than parties."
diff --git a/definitions/src/Control/Protocol/Example/Command.hs b/definitions/src/Control/Protocol/Example/Command.hs
deleted file mode 100644
index 375db8b2ff..0000000000
--- a/definitions/src/Control/Protocol/Example/Command.hs
+++ /dev/null
@@ -1,38 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE EmptyCase #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE InstanceSigs #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TemplateHaskell #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
-
-module Control.Protocol.Example.Command where
-
-import Control.Protocol
-import Data.Singletons.TH
-
-$( singletons
-     [d|
-       data Party = Recipient | Broker | Sender
-         deriving (Show, Eq)
-
-       data ChannelState
-         = None
-         | Ready
-         | Busy
-         deriving (Show, Eq)
-       |]
- )
-
-data MyCommand :: Command Party ChannelState where
-  Create :: MyCommand '(Recipient, None, Ready) '(Broker, None, Ready) ()
-  Notify :: MyCommand '(Recipient, Ready, Ready) '(Sender, None, Ready) ()
-  Send :: String -> MyCommand '(Sender, Ready, Ready) '(Broker, Ready, Busy) ()
-  Forward :: MyCommand '(Broker, Busy, Ready) '(Recipient, Ready, Ready) String
-
-type MyProtocol = Protocol MyCommand '[Recipient, Broker, Sender]
diff --git a/definitions/src/Control/Protocol/Example/Scenario.hs b/definitions/src/Control/Protocol/Example/Scenario.hs
deleted file mode 100644
index 51d7056361..0000000000
--- a/definitions/src/Control/Protocol/Example/Scenario.hs
+++ /dev/null
@@ -1,27 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE RebindableSyntax #-}
-{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
-
-module Control.Protocol.Example.Scenario where
-
-import Control.Protocol
-import Control.Protocol.Example.Command
-import Control.XMonad.Do
-import Data.Singletons
-import Prelude hiding ((>>), (>>=))
-
-r :: Sing Recipient
-r = SRecipient
-
-b :: Sing Broker
-b = SBroker
-
-s :: Sing Sender
-s = SSender
-
-scenario :: String -> MyProtocol '[None, None, None] '[Ready, Ready, Ready] String
-scenario str = do
-  r ->: b $ Create
-  r ->: s $ Notify
-  s ->: b $ Send str
-  b ->: r $ Forward
diff --git a/definitions/src/Simplex/Messaging/Connection.hs b/definitions/src/Simplex/Messaging/Connection.hs
index b6c924d8b4..6c994fab80 100644
--- a/definitions/src/Simplex/Messaging/Connection.hs
+++ b/definitions/src/Simplex/Messaging/Connection.hs
@@ -1 +1,70 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
+
 module Simplex.Messaging.Connection where
+
+import Data.Kind
+import Data.Text
+import Data.Type.Bool (type (||))
+import Data.Type.Equality (type (==))
+import Simplex.Messaging.Core
+import Simplex.Messaging.Types hiding (Invitation)
+
+-- | 'Connection' for all participants
+data Connection (p :: Party) (s :: ConnState) :: Type where
+  -- | no connection with this ID, used by all parties
+  NoConnection ::
+    ConnId ->
+    Connection p None
+  -- | connection created by the broker
+  ConnRcpNew ::
+    (s == New || s == Pending) ~ True =>
+    ClientConn ->
+    SenderConnId ->
+    PrivateKey -> -- key to decrypt messages from sender
+    PublicKey -> -- key for sender to encrypt messages to recipient
+    Connection Recipient s
+  -- | After sender confirmed connection:
+  --     * added sender's key for the broker (inside Conn)
+  --     * removed PublicKey previously sent to sender
+  ConnRcpConfirmed ::
+    ClientConn ->
+    Conn -> -- sender's connection info
+    PrivateKey -> -- key to decrypt messages from the sender
+    Connection Recipient Confirmed
+  -- | Connection is secured and can be used by the sender or it is disabled.
+  -- All sender connection information is removed now.
+  ConnRcp ::
+    (s == Secured || s == Disabled) ~ True =>
+    ClientConn ->
+    PrivateKey -> -- to decrypt messages from sender
+    Connection Recipient s
+  ConnSnd ::
+    (HasState Sender s, (s == None) ~ False) =>
+    ClientConn ->
+    PublicKey -> -- to encrypt messages to recipient
+    Connection Sender s
+  ConnBrkNew ::
+    Conn ->
+    SenderConnId ->
+    Connection Broker New
+  ConnBrk ::
+    (s == Secured || s == Disabled) ~ True =>
+    {recipient :: Conn, sender :: Conn} ->
+    Connection Broker s
+
+data Conn = Conn
+  { connId :: ConnId,
+    brokerVerifyKey :: PublicKey
+  }
+
+data ClientConn = ClientConn
+  { connId :: ConnId,
+    brokerVerifyKey :: PublicKey,
+    brokerKey :: PrivateKey,
+    brokerUri :: Text
+  }
diff --git a/definitions/src/Simplex/Messaging/Scenarios.hs b/definitions/src/Simplex/Messaging/Scenarios.hs
index 233ea51c7e..8b7293cd7f 100644
--- a/definitions/src/Simplex/Messaging/Scenarios.hs
+++ b/definitions/src/Simplex/Messaging/Scenarios.hs
@@ -30,7 +30,7 @@ establishConnection :: SimplexProtocol '[None, None, None] '[Secured, Secured, S
 establishConnection = do
   r ->: b $ CreateConn "BODbZxmtKUUF1l8pj4nVjQ"
   r ->: b $ Subscribe "RU"
-  r ->: s $ SendInvite "invitation RU" -- invitation - TODo
+  r ->: s $ SendInvite Invitation {connId = "SU"}
   s ->: b $ ConfirmConn "SU" "encrypted"
   b ->: r $ PushConfirm "RU" Message {msgId = "abc", msg = "XPaVEVNunkYKqqK0dnAT5Q"}
   r ->: b $ SecureConn "RU" "XPaVEVNunkYKqqK0dnAT5Q"
diff --git a/definitions/src/Simplex/Messaging/Types.hs b/definitions/src/Simplex/Messaging/Types.hs
index e582de8527..c8cc9e1772 100644
--- a/definitions/src/Simplex/Messaging/Types.hs
+++ b/definitions/src/Simplex/Messaging/Types.hs
@@ -6,63 +6,64 @@ module Simplex.Messaging.Types where
 
 import Data.Aeson
 import Data.String
+import Data.Text
 import GHC.Generics
 
-newtype CreateConnRequest
-  = CreateConnRequest
-      { recipientKey :: Key
-      }
+newtype CreateConnRequest = CreateConnRequest
+  { recipientKey :: Key
+  }
   deriving (Eq, Show, Generic, ToJSON, FromJSON)
 
 instance IsString CreateConnRequest where
   fromString = CreateConnRequest
 
-data CreateConnResponse
-  = CreateConnResponse
-      { recipientId :: String,
-        senderId :: String
-      }
+data CreateConnResponse = CreateConnResponse
+  { recipientId :: String,
+    senderId :: String
+  }
   deriving (Show, Generic, ToJSON, FromJSON)
 
-newtype SecureConnRequest
-  = SecureConnRequest
-      { senderKey :: Key
-      }
+newtype SecureConnRequest = SecureConnRequest
+  { senderKey :: Key
+  }
   deriving (Show, Generic, ToJSON, FromJSON)
 
 instance IsString SecureConnRequest where
   fromString = SecureConnRequest
 
-data Message
-  = Message
-      { msgId :: MessageId,
-        ts :: TimeStamp,
-        msg :: Encrypted -- TODO make it Text
-      }
+data Message = Message
+  { msgId :: MessageId,
+    ts :: TimeStamp,
+    msg :: Encrypted -- TODO make it Text
+  }
   deriving (Show, Generic, ToJSON, FromJSON)
 
-data MessagesResponse
-  = MessagesResponse
-      { messages :: [Message],
-        nextMessageId :: Maybe Base64EncodedString
-      }
+data MessagesResponse = MessagesResponse
+  { messages :: [Message],
+    nextMessageId :: Maybe Base64EncodedString
+  }
   deriving (Show, Generic, ToJSON, FromJSON)
 
-newtype SendMessageRequest
-  = SendMessageRequest
-      { msg :: Base64EncodedString
-      }
+newtype SendMessageRequest = SendMessageRequest
+  { msg :: Base64EncodedString
+  }
   deriving (Show, Generic, ToJSON, FromJSON)
 
 instance IsString SendMessageRequest where
   fromString = SendMessageRequest
 
-type Invitation = Base64EncodedString -- TODO define
+data Invitation = Invitation
+  { connId :: ConnId,
+    brokerUri :: Text,
+    encryptKey :: PublicKey
+  }
 
 type Key = Base64EncodedString -- deprecated, not to be used
 
 type PublicKey = Base64EncodedString
 
+type PrivateKey = Base64EncodedString
+
 type ConnId = Base64EncodedString
 
 type SenderConnId = Base64EncodedString
diff --git a/definitions/stack.yaml b/definitions/stack.yaml
index 491179a77c..28dee0f81e 100644
--- a/definitions/stack.yaml
+++ b/definitions/stack.yaml
@@ -41,6 +41,7 @@ packages:
 #
 extra-deps:
   - freer-indexed-0.1.0.0@sha256:b247be91b8ad2154fe1a514dec7c6a2553281d89325f0bc213d1d832d4c1a0e9,3007
+  - protocol-0.1.0.1@sha256:1e95952ba8fc17bbd6c1e4cf1e2993590a90ab938c30c6e530ad0f3ba4ec1a8c,1598
 # Override default flag values for local packages and extra-deps
 # flags: {}
 
diff --git a/specification/Simplex/Messaging/Protocol.idr b/specification/Simplex/Messaging/Protocol.idr
deleted file mode 100644
index fbf7a5b0ba..0000000000
--- a/specification/Simplex/Messaging/Protocol.idr
+++ /dev/null
@@ -1,303 +0,0 @@
-module Simplex.Messaging.Protocol
-
-%access public export
-
-data Participant = Recipient | Broker | Sender
-
-data Client : Participant -> Type where
-  CRecipient : Client Recipient
-  CSender    : Client Sender
-
-Key : Type
-Key = String
-
-PrivateKey : Type
-PrivateKey = String
-
-
--- Data structures for participants to store and pass connection information
-
-data Conn : Type where   -- connection info shared between a client and broker
-  MkConn : (id : String) -- connection ID to identify it with the broker
-        -> (key : Key)   -- public key for broker to verify commands
-        -> Conn
-
-record ClientConn where
-  constructor MkClientConn
-  conn   : Conn   -- same info that broker has for this client
-  label  : String -- label for the client to identify connection
-  broker : String -- broker URI
-  brokerPrivateKey : PrivateKey -- private key to sign commands to broker
-
-newClientConn : ClientConn
-newClientConn = MkClientConn (MkConn "" "") "" "" ""
-
-record RcpConn where -- recipient connection data
-  constructor MkRcpConn
-  clientConn       : ClientConn
-  senderPrivateKey : PrivateKey -- private key to decrypt sender messages
-
-newRcpConn : RcpConn
-newRcpConn = MkRcpConn newClientConn ""
-
-record Invitation where -- out of band message to sender inviting to connect
-  constructor MkInvitation
-  conn   : Conn
-  broker : String
-  senderKey : Key -- public key for sender to encrypt messages
-
-newInvitation : Invitation
-newInvitation = MkInvitation (MkConn "" "") "" ""
-
-record SndConn where -- sender connection data
-  constructor MkSndConn
-  clientConn : ClientConn
-  senderKey  : Key -- public key for sender to encrypt messages
-
-newSndConn : SndConn
-newSndConn = MkSndConn newClientConn ""
-
-
--- connection states for all participants
-
-data ConnectionState =  -- connection states for all participants
-            New         -- (participants: all) connection created (or received from sender)
-            | Pending   -- (recipient) sent to sender out-of-band
-            | Confirmed -- (recipient) confirmed by sender with the broker
-            | Secured   -- (all) secured with the broker
-            | Disabled  -- (broker, recipient) disabled with the broker by recipient
-            | Drained   -- (broker, recipient) drained (no messages)
-            | Null      -- (all) not available or removed from the broker
-
--- broker connection states
-data BrokerCS : ConnectionState -> Type where
-  BNew      : BrokerCS New
-  BSecured  : BrokerCS Secured
-  BDisabled : BrokerCS Disabled
-  BDrained  : BrokerCS Drained
-  BNull     : BrokerCS Null
-
--- sender connection states
-data SenderCS : ConnectionState -> Type where
-  SNew       : SenderCS New
-  SConfirmed : SenderCS Confirmed
-  SSecured   : SenderCS Secured
-  SNull      : SenderCS Null
-
--- allowed participant connection states
-data HasState : (p : Participant) -> (s : ConnectionState) -> Type where
-  BHasState : {auto prf : BrokerCS s} -> HasState Broker s
-  RHasState : HasState Recipient s
-  SHasState : {auto prf : SenderCS s} -> HasState Sender s
-
-
--- established connection states (used by broker and recipient)
-data EstablishedState : ConnectionState -> Type where
-  ESecured  : EstablishedState Secured
-  EDisabled : EstablishedState Disabled
-  EDrained  : EstablishedState Drained
-
-
--- dependent types to represent connections for all participants
-
-data BrokerConn : (state : ConnectionState)
-               -> {auto prf : HasState Broker state}
-               -> Type where
-  BCNew      : (recipient : Conn) -> (senderId : String) -> BrokerConn New
-  MkBrkConn  : (state : ConnectionState)
-            -> (recipient : Conn)
-            -> (sender : Conn)
-            -> {auto prf : HasState Broker state}
-            -> {auto prf : EstablishedState state}
-            -> BrokerConn state
-  -- 3 constructors below are equivalent to MkBrkConn with some state
-  BCSecured  : (recipient : Conn) -> (sender : Conn) -> BrokerConn Secured
-  BCDisabled : (recipient : Conn) -> (sender : Conn) -> BrokerConn Disabled
-  BCDrained  : (recipient : Conn) -> (sender : Conn) -> BrokerConn Drained
-  --
-  BCNull     : (id : String) -> BrokerConn Null
-
-
--- good broker connection sample
-goodBrkConn : BrokerConn Secured
-goodBrkConn = MkBrkConn Secured (MkConn "1" "1") (MkConn "2" "2")
-
--- bad broker connection sample - does not type check
--- badBrkConn : BrokerConn Null
--- badBrkConn = BCEstablished Null (MkConn "1" "1") (MkConn "2" "2")
-
-
-data RecipientConn : (state : ConnectionState) -> Type where
-  RCNew       : (conn : RcpConn) -> (sender : Invitation) -> RecipientConn New
-  RCPending   : (conn : RcpConn) -> (sender : Invitation) -> RecipientConn Pending
-  RCConfirmed : (conn : RcpConn) -> (sender : Conn) -> RecipientConn Confirmed
-  MkRecipientConn   : (state : ConnectionState)
-                   -> (conn : RcpConn)
-                   -> {auto prf : EstablishedState state}
-                   -> RecipientConn state
-  -- 3 constructors below are equivalent to MkRcpConn with some state
-  RCSecured   : (conn : RcpConn) -> RecipientConn Secured
-  RCDisabled  : (conn : RcpConn) -> RecipientConn Disabled
-  RCDrained   : (conn : RcpConn) -> RecipientConn Drained
-  --
-  RCNull      : (conn : RcpConn) -> RecipientConn Null
-
--- recipient connection sample
-goodRcpConn : RecipientConn Secured
-goodRcpConn = MkRecipientConn Secured (record
-                                        { clientConn = record
-                                                        { conn   = MkConn "1" "1"
-                                                        , label  = "label"
-                                                        , broker = "broker"
-                                                        , brokerPrivateKey = "2" }
-                                                       newClientConn
-                                        , senderPrivateKey = "3" }
-                                       newRcpConn)
-
-
-data SenderConn : (state : ConnectionState)
-               -> {auto prf : HasState Sender state}
-               -> Type where
-  SCNew       : (conn : Invitation) -> SenderConn New
-  SCConfirmed : (conn : SndConn) -> SenderConn Confirmed
-  SCSecured   : (conn : SndConn) -> SenderConn Secured
-  SCNull      : (conn : SndConn) -> SenderConn Null
-
--- sender connection sample
-goodSndConn : SenderConn Secured
-goodSndConn = SCSecured (record
-                          { clientConn = record
-                                          { conn   = MkConn "1" "1"
-                                          , label  = "label"
-                                          , broker = "broker"
-                                          , brokerPrivateKey = "2" }
-                                         newClientConn
-                          , senderKey = "3" }
-                         newSndConn)
-
-
--- protocol commands that participants send in relation to specific connection
-data Result : (a : Type) -> Type where
-  OK   : a -> Result a
-  Deny : Result a -- access restriction, not some arbitrary error
-  Err  : String -> Result a -- another error
-
-record BrkCreateConnRes where
-  constructor MkBrkCreateConnRes
-  connId : String
-  senderConnId : String
-
-Message : Type
-Message = String
-
--- operator to define connection state change based on the result
-infixl 7 <==>, <==|
-prefix 6 />>, >>>
-
-data RBConnState : Type where
-  (<==>) : (recipient : ConnectionState)
-        -> (broker    : (ConnectionState, Nat)) -- number of messages in connection
-        -> {auto prf  : (\(s, _) => HasState Broker s) broker}
-        -> RBConnState
-
-data AllConnState : Type where
-  (<==|) : (rcpBrk : RBConnState)
-        -> (sender : ConnectionState)
-        -> {auto prf : HasState Sender sender}
-        -> AllConnState
-
-(/>>) : AllConnState
-     -> (AllConnState -> Result a -> AllConnState)
-(/>>) s' = \s, x => case x of
-                      OK _  => s'
-                      Deny  => s
-                      Err _ => s
-
-(>>>) : AllConnState
-     -> (AllConnState -> Result a -> AllConnState)
-(>>>) s = \_, _ => s
-
-data Command : (ty : Type)
-            -> (Participant, Participant)
-            -> (state : AllConnState)
-            -> ((state : AllConnState) -> Result ty -> AllConnState)
-            -> Type where
-
-  CreateConn  : (recipientBrokerKey : Key)
-             -> {auto prf : HasState Sender s}
-             -> Command BrkCreateConnRes
-                  (Recipient, Broker)
-                  (Null <==> (Null, 0) <==| s)
-                  (>>> New <==> (New, 0)  <==| s)
-
-  Subscribe   : Command () (Recipient, Broker) state (>>> state) -- to improve
-
-  SendInvite  : Invitation
-             -> {auto prf : HasState Broker s}
-             -> Command ()
-                  (Recipient, Sender)
-                  (New <==> (s, n) <==| Null)
-                  (>>> Pending <==> (s, n) <==| New)
-
-  ConfirmConn : (senderBrokerKey : Key)
-             -> Command ()
-                  (Sender, Broker)
-                  (s <==> (New, n) <==| New)
-                  (>>> s <==> (New, 1 + n) <==| Confirmed)
-
-  PushConfirm : {auto prf : HasState Sender s}
-             -> Command ()
-                  (Broker, Recipient)
-                  (Pending <==> (New, 1 + n) <==| s)
-                  (>>> Confirmed <==> (New, n) <==| s)
-
-  SecureConn  : (senderBrokerKey : Key)
-             -> {auto prf : HasState Sender s}
-             -> Command ()
-                  (Recipient, Broker)
-                  (Confirmed <==> (New, n) <==| s)
-                  (>>> Secured <==> (Secured, n) <==| s)
-
-  SendWelcome : {auto prf : HasState Broker bs}
-             -> Command ()
-                  (Sender, Broker)
-                  (rs <==> (Secured, n) <==| Confirmed)
-                  (>>> rs <==> (Secured, 1 + n) <==| Secured)
-
-  PushWelcome : {auto prf : HasState Sender s}
-             -> Command ()
-                  (Broker, Recipient)
-                  (Secured <==> (Secured, 1 + n) <==| s)
-                  (>>> Secured <==> (Secured, n) <==| s)
-
-  SendMsg     : Message
-             -> Command ()
-                  (Sender, Broker)
-                  (rs <==> (Secured, n) <==| Secured)
-                  (>>> rs <==> (Secured, 1 + n) <==| Secured)
-
-  PushMsg     : {auto prf : HasState Sender s}
-             -> Command ()
-                  (Broker, Recipient)
-                  (Secured <==> (Secured, n) <==| s)
-                  (>>> Secured <==> (Secured, n) <==| s)
-
-  DeleteMsg   : {auto prf : HasState Sender s}
-             -> Command ()
-                  (Recipient, Broker)
-                  (Secured <==> (Secured, 1 + n) <==| s)
-                  (>>> Secured <==> (Secured, n) <==| s)
-
-
-  Pure  : (res : Result a) -> Command a ps state state_fn
-  (>>=) : Command a ps1 state1 state2_fn
-          -> ((res : Result a) -> Command b ps2 (state2_fn state1 res) state3_fn)
-          -> Command b (fst ps1, snd ps2) state1 state3_fn
-
-
-infix 5 &:
-(&:) : (p : Participant)
-    -> Command a ps state1 state2_fn
-    -> {auto prf : p = fst ps}
-    -> Command a ps state1 state2_fn
-(&:) _ c = c
diff --git a/specification/Simplex/Messaging/Scenarios.idr b/specification/Simplex/Messaging/Scenarios.idr
deleted file mode 100644
index 8469a605a6..0000000000
--- a/specification/Simplex/Messaging/Scenarios.idr
+++ /dev/null
@@ -1,20 +0,0 @@
-module Simplex.Messaging.Scenarios
-
-import Simplex.Messaging.Protocol
-
-establishConnection : Command ()
-                        (Recipient, Broker)
-                        (Null <==> (Null, 0) <==| Null)
-                        (>>> Secured <==> (Secured, 0) <==| Secured)
-establishConnection = do
-  Recipient &: CreateConn "recipient's public key for broker"
-  Recipient &: Subscribe
-  Recipient &: SendInvite newInvitation
-  Sender    &: ConfirmConn "sender's public key for broker"
-  Broker    &: PushConfirm
-  Recipient &: SecureConn "sender's public key for broker"
-  Sender    &: SendWelcome
-  Broker    &: PushWelcome
-  Sender    &: SendMsg "Hello"
-  Broker    &: PushMsg
-  Recipient &: DeleteMsg