diff --git a/AVM/Authorization.lean b/AVM/Authorization.lean
index 94d95e5f..5d89e011 100644
--- a/AVM/Authorization.lean
+++ b/AVM/Authorization.lean
@@ -1,5 +1,8 @@
 import Mathlib.Data.Fintype.Basic
 import Prelude
+import AVM.Message.Data
+
+namespace AVM
 
 structure PublicKey where
   key : Nat
@@ -21,19 +24,20 @@ def PrivateKey.universal : PrivateKey where
 -- mock function
 private def checkKey (pub : PublicKey) (priv : PrivateKey) : Bool := pub.key == priv.key
 
-structure Signature {A : Type u} (msg : A) : Type u where
-  msg : A
+structure Signature where
+  user : PublicKey
   private signature : PrivateKey
 
 -- Mock function that returns the `raw` bytes of the signature
-def Signature.raw {A : Type u} (msg : A) (_s : Signature msg ) : Nat := 0
+def Signature.raw (_s : Signature) : Nat := 0
 
-instance {A B} (msgA : A) (msgB : B) : HBEq (Signature msgA) (Signature msgB) where
-  hbeq a b := a.raw == b.raw
+instance : BEq Signature where
+  beq a b := a.raw == b.raw
 
-def Signature.sign {A : Type u} (msg : A) (key : PrivateKey) : Signature msg where
+def Signature.sign {lab : Ecosystem.Label} (_msg : MessageData lab) (key : PrivateKey) (pub : PublicKey) : Signature where
+  user := pub
   signature := key
-  msg
 
 -- mock function
-def checkSignature {A : Type u} {msg : A} (sig : Signature msg) (pub : PublicKey) : Bool := checkKey pub sig.signature
+def checkSignature {lab : Ecosystem.Label} (_msg : MessageData lab) (sigs : List Signature) (pub : PublicKey)  : Bool :=
+  sigs.any (fun sig => sig.user == pub && checkKey pub sig.signature)
diff --git a/AVM/Class/Label.lean b/AVM/Class/Label.lean
index a523bea8..bfe01a48 100644
--- a/AVM/Class/Label.lean
+++ b/AVM/Class/Label.lean
@@ -2,7 +2,6 @@ import Anoma.Resource
 import Prelude
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Data.FinEnum
-import AVM.Authorization
 
 abbrev AVM.ObjectId := Anoma.ObjectId
 
@@ -34,9 +33,6 @@ structure Label : Type 1 where
 
   ConstructorId : Type
   ConstructorArgs : ConstructorId -> SomeType
-  ConstructorSignatureId : ConstructorId → Type := fun _ => Empty
-  ConstructorSignatureIdEnum : (s : ConstructorId) → FinEnum (ConstructorSignatureId s)
-    := by intro s; cases s <;> infer_instance
   [constructorsEnum : FinEnum ConstructorId]
   [constructorsRepr : Repr ConstructorId]
   [constructorsBEq : BEq ConstructorId]
@@ -44,9 +40,6 @@ structure Label : Type 1 where
 
   DestructorId : Type := Empty
   DestructorArgs : DestructorId -> SomeType := fun _ => ⟨PUnit⟩
-  DestructorSignatureId : DestructorId → Type := fun _ => Empty
-  DestructorSignatureIdEnum : (s : DestructorId) → FinEnum (DestructorSignatureId s)
-    := by intro s; cases s <;> infer_instance
   [destructorsEnum : FinEnum DestructorId]
   [destructorsRepr : Repr DestructorId]
   [destructorsBEq : BEq DestructorId]
@@ -54,9 +47,6 @@ structure Label : Type 1 where
 
   MethodId : Type
   MethodArgs : MethodId -> SomeType
-  MethodSignatureId : MethodId → Type := fun _ => Empty
-  MethodSignatureIdEnum : (s : MethodId) → FinEnum (MethodSignatureId s)
-    := by intro s; cases s <;> infer_instance
   [methodsEnum : FinEnum MethodId]
   [methodsRepr : Repr MethodId]
   [methodsBEq : BEq MethodId]
@@ -87,12 +77,6 @@ inductive Label.MemberId (lab : Class.Label) : Type where
   | methodId (methodId : lab.MethodId) : MemberId lab
   | upgradeId : MemberId lab
 
-abbrev Label.MemberId.SignatureId {lab : Class.Label} : Label.MemberId lab → Type
-  | .methodId m => lab.MethodSignatureId m
-  | .destructorId m => lab.DestructorSignatureId m
-  | .constructorId m => lab.ConstructorSignatureId m
-  | .upgradeId => Empty
-
 instance Label.MemberId.instHashable {lab : Class.Label} : Hashable (Class.Label.MemberId lab) where
   hash l := Hashable.Mix.run do
     mix lab
@@ -163,34 +147,6 @@ def Label.MemberId.Args {lab : Class.Label} (memberId : MemberId lab) : SomeType
   | methodId c => lab.MethodArgs c
   | upgradeId => ⟨PUnit⟩
 
-abbrev Label.MemberId.Signatures
-  {lab : Class.Label}
-  (f : MemberId lab)
-  (args : f.Args.type)
-  : Type :=
-  f.SignatureId → Signature (f, args)
-
-abbrev Label.MethodId.Signatures
-  {lab : Class.Label}
-  (f : lab.MethodId)
-  (args : f.Args.type)
-  : Type :=
-  MemberId.methodId f |>.Signatures args
-
-abbrev Label.ConstructorId.Signatures
-  {lab : Class.Label}
-  (f : lab.ConstructorId)
-  (args : f.Args.type)
-  : Type :=
-  MemberId.constructorId f |>.Signatures args
-
-abbrev Label.DestructorId.Signatures
-  {lab : Class.Label}
-  (f : lab.DestructorId)
-  (args : f.Args.type)
-  : Type :=
-  MemberId.destructorId f |>.Signatures args
-
 instance Label.hasTypeRep : TypeRep Label where
   rep := Rep.atomic "AVM.Class.Label"
 
diff --git a/AVM/Class/Member.lean b/AVM/Class/Member.lean
index 5e36740d..1674d798 100644
--- a/AVM/Class/Member.lean
+++ b/AVM/Class/Member.lean
@@ -7,20 +7,20 @@ structure Constructor {lab : Ecosystem.Label} (cid : lab.ClassId) (constrId : ci
   body : constrId.Args.type → Program.{0} lab.toScope (ObjectData cid)
   /-- Extra constructor logic. The constructor invariant is combined with
       auto-generated constructor body constraints to create the constructor logic. -/
-  invariant : (args : constrId.Args.type) → constrId.Signatures args →  Bool
+  invariant : (msg : Message lab) → (args : constrId.Args.type) → Bool
 
 structure Destructor {lab : Ecosystem.Label} (cid : lab.ClassId) (destructorId : cid.label.DestructorId) : Type 1 where
   /-- Destructor call body. -/
   body : (self : Object cid) → destructorId.Args.type → Program.{0} lab.toScope PUnit
   /-- Extra destructor logic. -/
-  invariant : (self : Object cid) → (args : destructorId.Args.type) → destructorId.Signatures args → Bool
+  invariant : (msg : Message lab) → (self : Object cid) → (args : destructorId.Args.type) → Bool
 
 structure Method {lab : Ecosystem.Label} (cid : lab.ClassId) (methodId : cid.label.MethodId) : Type 1 where
   /-- Method call body. -/
   body : (self : Object cid) → methodId.Args.type → Program lab.toScope (Object cid)
   /-- Extra method logic. The method invariant is combined with auto-generated
       method body constraints to create the method logic. -/
-  invariant : (self : Object cid) → (args : methodId.Args.type) → methodId.Signatures args → Bool
+  invariant : (msg : Message lab) → (self : Object cid) → (args : methodId.Args.type) → Bool
 
 /-- A class member is a constructor, a destructor or a method. -/
 inductive Member {lab : Ecosystem.Label} (cid : lab.ClassId) where
diff --git a/AVM/Class/Translation/Logics.lean b/AVM/Class/Translation/Logics.lean
index b7b4c9d4..f9c03103 100644
--- a/AVM/Class/Translation/Logics.lean
+++ b/AVM/Class/Translation/Logics.lean
@@ -3,21 +3,6 @@ import AVM.Message
 import AVM.Logic
 import AVM.Ecosystem
 
-namespace AVM.Logic
-
-def classLogicRef {lab : Ecosystem.Label} (classId : lab.ClassId) : Anoma.LogicRef :=
-  classId.label.logicRef
-
-def trivialLogicRef : Anoma.LogicRef := Anoma.LogicRef.mk "Anoma.TrivialLogic"
-
-def trivialLogic : Anoma.Logic :=
-  { reference := trivialLogicRef,
-    function := fun _ => true }
-
-abbrev builtinLogics : List Anoma.Logic := [trivialLogic]
-
-end AVM.Logic
-
 namespace AVM.Program
 
 structure MessageValue (lab : Ecosystem.Label) where
@@ -78,7 +63,7 @@ def checkMessageResourceValues {lab : Ecosystem.Label} (vals : List (Program.Mes
   List.all₂
     (fun val res =>
       let try msg : Message lab := Message.fromResource res
-      msg.id == val.id && msg.args === val.args && msg.logicRef == val.logicRef)
+      msg.data.id == val.id && msg.data.args === val.args)
     vals
     resMsgs
 
@@ -93,16 +78,15 @@ def MultiMethod.Message.logicFun
   (msg : Message lab)
   (args : Logic.Args)
   : Bool :=
-  check h : msg.id == .multiMethodId multiId
-  let fargs : multiId.Args.type := cast (by simp! [eq_of_beq h]) msg.args
+  check h : msg.data.id == .multiMethodId multiId
+  let fargs : multiId.Args.type := cast (by simp! [eq_of_beq h]) msg.data.args
   let consumedResObjs := Logic.selectObjectResources args.consumed
   let createdResObjs := Logic.selectObjectResources args.created
   let argsConsumedSelves := consumedResObjs.take multiId.numObjectArgs
   let try argsConsumedObjects : multiId.Selves := Label.MultiMethodId.ConsumedToSelves argsConsumedSelves
+  check method.invariant msg argsConsumedObjects fargs
   let prog := method.body argsConsumedObjects fargs
-  let signatures := cast (by grind only) msg.signatures
-  check method.invariant argsConsumedObjects fargs signatures
-  let try vals : prog.params.Product := tryCast msg.vals
+  let try vals : prog.params.Product := tryCast msg.data.vals
   let res : MultiMethodResult multiId := prog.value vals
   let valsObjs := prog.objects vals
   let fetchedObjValues := valsObjs.map (·.toObjectValue)
@@ -160,11 +144,10 @@ private def Constructor.Message.logicFun
   (msg : Message lab)
   (args : Logic.Args)
   : Bool :=
-  check h : msg.id == .classMember (Label.MemberId.constructorId constrId)
-  let argsData : constrId.Args.type := cast (by simp! [eq_of_beq h]) msg.args
-  let signatures : constrId.Signatures argsData := cast (by grind only) msg.signatures
+  check h : msg.data.id == .classMember (Label.MemberId.constructorId constrId)
+  let argsData : constrId.Args.type := cast (by simp! [eq_of_beq h]) msg.data.args
   let body := constr.body argsData
-  let try vals : body.params.Product := tryCast msg.vals
+  let try vals : body.params.Product := tryCast msg.data.vals
   let newObjData := body.value vals
   let consumedResObjs := Logic.selectObjectResources args.consumed
   let createdResObjs := Logic.selectObjectResources args.created
@@ -182,7 +165,7 @@ private def Constructor.Message.logicFun
     && Logic.checkResourcesEphemeral [consumedObjRes]
     && Logic.checkResourcesPersistent createdResObjs
     && Logic.checkResourcesPersistent consumedFetchedResObjs
-    && constr.invariant argsData signatures
+    && constr.invariant msg argsData
 
 /-- Creates a message logic function for a given destructor. -/
 private def Destructor.Message.logicFun
@@ -193,16 +176,15 @@ private def Destructor.Message.logicFun
   (msg : Message lab)
   (args : Logic.Args)
   : Bool :=
-  check h : msg.id == .classMember (Label.MemberId.destructorId destructorId)
-  let argsData := cast (by simp! [eq_of_beq h]) msg.args
-  let signatures : destructorId.Signatures argsData := cast (by grind only) msg.signatures
+  check h : msg.data.id == .classMember (Label.MemberId.destructorId destructorId)
+  let argsData := cast (by simp! [eq_of_beq h]) msg.data.args
   let consumedResObjs := Logic.selectObjectResources args.consumed
   let createdResObjs := Logic.selectObjectResources args.created
   let! (selfRes :: _) := consumedResObjs
   let! (createdResObj :: createdFetchedResObjs) := createdResObjs
   let try selfObj : Object classId := Object.fromResource selfRes
   let body := destructor.body selfObj argsData
-  let try vals : body.params.Product := tryCast msg.vals
+  let try vals : body.params.Product := tryCast msg.data.vals
   let messageValues := Program.messageValues body vals
   let createdResMsgs := Logic.selectMessageResources args.created
   let valsObjs := body.objects vals
@@ -214,7 +196,7 @@ private def Destructor.Message.logicFun
     && Logic.checkResourcesPersistent consumedResObjs
     && Logic.checkResourcesEphemeral [createdResObj]
     && Logic.checkResourcesPersistent createdFetchedResObjs
-    && destructor.invariant selfObj argsData signatures
+    && destructor.invariant msg selfObj argsData
 
 private def Method.Message.logicFun
   {lab : Ecosystem.Label}
@@ -224,16 +206,15 @@ private def Method.Message.logicFun
   (msg : Message lab)
   (args : Logic.Args)
   : Bool :=
-  check h : msg.id == .classMember (Label.MemberId.methodId methodId)
-  let argsData : methodId.Args.type := cast (by simp! [eq_of_beq h]) msg.args
+  check h : msg.data.id == .classMember (Label.MemberId.methodId methodId)
+  let argsData : methodId.Args.type := cast (by simp! [eq_of_beq h]) msg.data.args
   let consumedResObjs := Logic.selectObjectResources args.consumed
   let createdResObjs := Logic.selectObjectResources args.created
   let! (selfRes :: _) := consumedResObjs
   let try selfObj : Object classId := Object.fromResource selfRes
   let body := method.body selfObj argsData
-  let try vals : body.params.Product := tryCast msg.vals
-  let signatures : methodId.Signatures argsData := cast (by grind only) msg.signatures
-  check method.invariant selfObj argsData signatures
+  let try vals : body.params.Product := tryCast msg.data.vals
+  check method.invariant msg selfObj argsData
   let createdObject : Object classId := body |>.value vals
   let messageValues := Program.messageValues body vals
   let createdResMsgs := Logic.selectMessageResources args.created
@@ -314,8 +295,8 @@ private def logicFun
       -- Note: the success of the `try` below ensures that the message is "legal"
       -- for the consumed objects - it is from the same ecosystem
       let try msg : Message lab := Message.fromResource consumedMessageResource
-      self.uid ∈ msg.recipients
-      && Member.logicFun eco msg.id msg args
+      self.uid ∈ msg.data.recipients
+      && Member.logicFun eco msg.data.id msg args
 
 /-- The class logic that is the Resource Logic of each resource corresponding to
   an object of this class. -/
diff --git a/AVM/Class/Translation/Messages.lean b/AVM/Class/Translation/Messages.lean
index 970289ee..7f9a78d7 100644
--- a/AVM/Class/Translation/Messages.lean
+++ b/AVM/Class/Translation/Messages.lean
@@ -1,7 +1,6 @@
-import AVM.Ecosystem.Label
+import AVM.Ecosystem
 import AVM.Class
 import AVM.Message
-import AVM.Class.Translation.Logics
 
 namespace AVM.Class
 
@@ -14,14 +13,15 @@ def Constructor.message
   (vals : Vals.type)
   (newId : ObjectId)
   (args : constrId.Args.type)
-  (signatures : Class.Label.MemberId.constructorId constrId |>.Signatures args)
+  (signatures : MessageData lab → List Signature)
   : Message lab :=
-  { id := .classMember (.constructorId constrId)
-    logicRef := Logic.trivialLogicRef
-    vals
-    args
-    signatures
-    recipients := [newId] }
+  let data : MessageData lab :=
+    { id := .classMember (.constructorId constrId)
+      vals
+      args
+      recipients := [newId] }
+  { data,
+    signatures := signatures data }
 
 def Destructor.message
   {lab : Ecosystem.Label}
@@ -32,14 +32,15 @@ def Destructor.message
   (vals : Vals.type)
   (selfId : ObjectId)
   (args : destrId.Args.type)
-  (signatures : Class.Label.MemberId.destructorId destrId |>.Signatures args)
+  (signatures : MessageData lab → List Signature)
   : Message lab :=
-  { id := .classMember (.destructorId destrId)
-    logicRef := Logic.trivialLogicRef
-    vals
-    args
-    signatures
-    recipients := [selfId] }
+  let data : MessageData lab :=
+    { id := .classMember (.destructorId destrId)
+      vals
+      args
+      recipients := [selfId] }
+  { data,
+    signatures := signatures data }
 
 def Method.message
   {lab : Ecosystem.Label}
@@ -50,27 +51,28 @@ def Method.message
   (vals : Vals.type)
   (selfId : ObjectId)
   (args : methodId.Args.type)
-  (signatures : Class.Label.MemberId.methodId methodId |>.Signatures args)
+  (signatures : MessageData lab → List Signature)
   : Message lab :=
-  { id := .classMember (.methodId methodId)
-    logicRef := Logic.trivialLogicRef
-    vals
-    args
-    signatures
-    recipients := [selfId] }
+  let data : MessageData lab :=
+    { id := .classMember (.methodId methodId)
+      vals
+      args
+      recipients := [selfId] }
+  { data,
+    signatures := signatures data }
 
 def Upgrade.message
   {lab : Ecosystem.Label}
   (classId : lab.ClassId)
   (selfId : ObjectId)
   : Message lab :=
-  { id := .classMember (classId := classId) .upgradeId
-    logicRef := Logic.trivialLogicRef
-    Vals := ⟨PUnit⟩
-    vals := PUnit.unit
-    args := .unit
-    signatures f := nomatch f
-    recipients := [selfId] }
+  let data : MessageData lab :=
+    { id := .classMember (classId := classId) .upgradeId
+      Vals := ⟨PUnit⟩
+      vals := PUnit.unit
+      args := .unit
+      recipients := [selfId] }
+  { data, signatures := []}
 
 end AVM.Class
 
@@ -82,17 +84,18 @@ def MultiMethod.message
   (method : MultiMethod multiId)
   (selves : multiId.Selves)
   (args : multiId.Args.type)
-  (signatures : multiId.Signatures args)
+  (signatures : MessageData lab → List Signature)
   (vals : (method.body selves args).params.Product)
   (data : MultiMethodData)
   (rands : MultiMethodRandoms data)
   : Message lab :=
-  { id := .multiMethodId multiId
-    logicRef := Logic.trivialLogicRef
-    Vals := ⟨(method.body selves args).params.Product⟩
-    vals
-    args
-    signatures
-    recipients :=
-      (Label.MultiMethodId.SelvesToVector selves (fun obj => obj.uid) |>.toList)
-        ++ rands.constructedNonces.toList.map (·.value) }
+  let data : MessageData lab :=
+    { id := .multiMethodId multiId
+      Vals := ⟨(method.body selves args).params.Product⟩
+      vals
+      args
+      recipients :=
+        (Label.MultiMethodId.SelvesToVector selves (fun obj => obj.uid) |>.toList)
+          ++ rands.constructedNonces.toList.map (·.value) }
+  { data,
+    signatures := signatures data }
diff --git a/AVM/Class/Translation/Tasks.lean b/AVM/Class/Translation/Tasks.lean
index 77aac00d..cdf54a57 100644
--- a/AVM/Class/Translation/Tasks.lean
+++ b/AVM/Class/Translation/Tasks.lean
@@ -160,7 +160,7 @@ private partial def Class.Constructor.task'
   (newId : ObjectId)
   (r : Nat)
   (args : constrId.Args.type)
-  (signatures : constrId.Signatures args)
+  (signatures : MessageData lab → List Signature)
   : Task' :=
   let body : Program.{1} lab.toScope (ULift (ObjectData classId)) := constr.body args |>.lift
   let mkActionData (rands : List Nat) (vals : body.params.Product) (newObjectData : ULift (ObjectData classId)) : ActionData :=
@@ -193,7 +193,7 @@ private partial def Class.Destructor.task'
   (r : Nat)
   (self : Object classId)
   (args : destructorId.Args.type)
-  (signatures : destructorId.Signatures args)
+  (signatures : MessageData lab → List Signature)
   : Task' :=
   let body : Program.{1} lab.toScope (ULift Unit) := destructor.body self args |>.lift
   let mkActionData (rands : List Nat) (vals : body.params.Product) (_ : ULift Unit) : ActionData :=
@@ -223,7 +223,7 @@ private partial def Class.Method.task'
   (r : Nat)
   (self : Object classId)
   (args : methodId.Args.type)
-  (signatures : methodId.Signatures args)
+  (signatures : MessageData lab → List Signature)
   : Task' :=
   let body : Program.{1} lab.toScope (ULift (Object classId)) := method.body self args |>.lift
   let mkActionData (rands : List Nat) (vals : body.params.Product) (lobj : ULift (Object classId)) : ActionData :=
@@ -274,7 +274,7 @@ partial def Ecosystem.MultiMethod.task'
   (method : Ecosystem.MultiMethod multiId)
   (selves : multiId.Selves)
   (args : multiId.Args.type)
-  (signatures : multiId.Signatures args)
+  (signatures : MessageData lab → List Signature)
   : Task' :=
   let body := method.body selves args
 
diff --git a/AVM/Ecosystem/Label/Base.lean b/AVM/Ecosystem/Label/Base.lean
index fe61eec4..85031335 100644
--- a/AVM/Ecosystem/Label/Base.lean
+++ b/AVM/Ecosystem/Label/Base.lean
@@ -1,5 +1,4 @@
 import AVM.Class.Label
-import AVM.Authorization
 
 namespace AVM.Ecosystem
 
@@ -20,9 +19,6 @@ structure Label : Type 1 where
   MultiMethodObjectArgNames : MultiMethodId → Type := fun _ => PUnit
   /-- Class identifiers for `self` arguments. -/
   MultiMethodObjectArgClass : {f : MultiMethodId} → MultiMethodObjectArgNames f → ClassId
-  MultiMethodSignatureId : MultiMethodId → Type := fun _ => Empty
-  MultiMethodSignatureIdEnum : (s : MultiMethodId) → FinEnum (MultiMethodSignatureId s)
-    := by intro s; cases s <;> infer_instance
   [ObjectArgNamesEnum (f : MultiMethodId) : FinEnum (MultiMethodObjectArgNames f)]
   [ObjectArgNamesBEq (f : MultiMethodId) : BEq (MultiMethodObjectArgNames f)]
   [multiMethodsFinite : FinEnum MultiMethodId]
@@ -102,11 +98,6 @@ namespace MultiMethodId
 abbrev Args {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : SomeType :=
   lab.MultiMethodArgs multiId
 
-abbrev SignatureId {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : Type := lab.MultiMethodSignatureId multiId
-
-abbrev Signatures {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) (args : multiId.Args.type) : Type :=
-  multiId.SignatureId → Signature (multiId, args)
-
 def ObjectArgNames {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : Type :=
   lab.MultiMethodObjectArgNames multiId
 
@@ -190,21 +181,11 @@ instance instLawfulBEq {lab : Ecosystem.Label} : LawfulBEq lab.MemberId where
       subst x; simp
     contradiction
 
-abbrev SignatureId (lab : Ecosystem.Label) : MemberId lab → Type
-  | .classMember m => m.SignatureId
-  | .multiMethodId m => m.SignatureId
-
 abbrev Args {lab : Ecosystem.Label} (memberId : MemberId lab) : SomeType.{0} :=
   match memberId with
   | multiMethodId f => lab.MultiMethodArgs f
   | classMember m => Class.Label.MemberId.Args m
 
-abbrev Signatures {lab : Ecosystem.Label} (mem : MemberId lab) (args : mem.Args.type)
-  : Type :=
-  match mem with
-  | .classMember m => m.Signatures args
-  | .multiMethodId m => m.Signatures args
-
 /-- The number of object arguments (selves) for this member ID. -/
 def numObjectArgs {lab : Ecosystem.Label} (memberId : MemberId lab) : Nat :=
   match memberId with
diff --git a/AVM/Ecosystem/Member.lean b/AVM/Ecosystem/Member.lean
index 9feccd42..8bd99d7e 100644
--- a/AVM/Ecosystem/Member.lean
+++ b/AVM/Ecosystem/Member.lean
@@ -96,4 +96,4 @@ structure Ecosystem.MultiMethod {lab : Ecosystem.Label} (multiId : lab.MultiMeth
   /-- Computes the result of a multiMethod call. See `MultiMethodResult`. -/
   body (selves : multiId.Selves) (args : multiId.Args.type) : Program.{1} lab.toScope (MultiMethodResult multiId)
   /-- Extra multiMethod logic. -/
-  invariant (selves : multiId.Selves) (args : multiId.Args.type) (signatures : multiId.Signatures args) : Bool
+  invariant (msg : Message lab) (selves : multiId.Selves) (args : multiId.Args.type) : Bool
diff --git a/AVM/Logic.lean b/AVM/Logic.lean
index 5f58da13..86c9712b 100644
--- a/AVM/Logic.lean
+++ b/AVM/Logic.lean
@@ -3,6 +3,7 @@ import Anoma
 import AVM.Object
 import AVM.Message
 import AVM.Action.DummyResource
+import AVM.Logic.Base
 
 namespace AVM.Logic
 
diff --git a/AVM/Logic/Base.lean b/AVM/Logic/Base.lean
new file mode 100644
index 00000000..73998243
--- /dev/null
+++ b/AVM/Logic/Base.lean
@@ -0,0 +1,15 @@
+import Anoma
+import AVM.Ecosystem.Label.Base
+
+namespace AVM.Logic
+
+def classLogicRef {lab : Ecosystem.Label} (classId : lab.ClassId) : Anoma.LogicRef :=
+  classId.label.logicRef
+
+def trivialLogicRef : Anoma.LogicRef := Anoma.LogicRef.mk "Anoma.TrivialLogic"
+
+def trivialLogic : Anoma.Logic :=
+  { reference := trivialLogicRef,
+    function := fun _ => true }
+
+abbrev builtinLogics : List Anoma.Logic := [trivialLogic]
diff --git a/AVM/Message.lean b/AVM/Message.lean
index 0d6f22fc..251c5aa4 100644
--- a/AVM/Message.lean
+++ b/AVM/Message.lean
@@ -2,6 +2,7 @@ import AVM.Class.Label
 import AVM.Ecosystem.Label
 import AVM.Ecosystem.Data
 import AVM.Authorization
+import AVM.Logic.Base
 
 namespace AVM
 
@@ -9,7 +10,7 @@ def SomeMessage.toResource (msg : SomeMessage) (nonce : Anoma.Nonce) : Anoma.Res
   { Val := ⟨PUnit⟩,
     Label := ⟨SomeMessage⟩,
     label := msg,
-    logicRef := msg.message.logicRef,
+    logicRef := Logic.trivialLogicRef,
     value := PUnit.unit,
     quantity := 1,
     nullifierKeyCommitment := default,
@@ -18,7 +19,6 @@ def SomeMessage.toResource (msg : SomeMessage) (nonce : Anoma.Nonce) : Anoma.Res
 
 def SomeMessage.fromResource (res : Anoma.Resource) : Option SomeMessage :=
   let try msg : SomeMessage := tryCast res.label
-  check (msg.message.logicRef == res.logicRef)
   some msg
 
 def Message.toResource {lab : Ecosystem.Label} (msg : Message lab) (nonce : Anoma.Nonce) : Anoma.Resource :=
@@ -30,3 +30,6 @@ def Message.fromResource {lab : Ecosystem.Label} (res : Anoma.Resource) : Option
 
 def Resource.isSomeMessage (res : Anoma.Resource) : Bool :=
   Option.isSome (SomeMessage.fromResource res)
+
+def Message.checkSignature {lab : Ecosystem.Label} (msg : Message lab) (pub : PublicKey)  : Bool :=
+  AVM.checkSignature msg.data msg.signatures pub
diff --git a/AVM/Message/Base.lean b/AVM/Message/Base.lean
index 4d77ec4c..32749e32 100644
--- a/AVM/Message/Base.lean
+++ b/AVM/Message/Base.lean
@@ -1,54 +1,27 @@
-import AVM.Ecosystem.Data
+import AVM.Message.Data
+import AVM.Authorization
 
 namespace AVM
 
 /-- A message is a communication sent from one object to another in the AVM. -/
 structure Message (lab : Ecosystem.Label) : Type 1 where
-  /-- The message ID. -/
-  id : lab.MemberId
-  {Vals : SomeType.{0}}
-  /-- Message parameter values. The message parameters are object resources and
-    generated random values that are used in the body of the call associated with
-    the message. These need to be provided in the message, because the
-    associated Resource Logic cannot fetch object resources from the Anoma
-    system or generate new object identifiers. -/
-  vals : Vals.type
-  /-- Resource logic reference for the message logic. -/
-  logicRef : Anoma.LogicRef
-  /-- The arguments of the message. -/
-  args : id.Args.type
-  /-- The signature of the arguments -/
-  signatures : id.Signatures args
-  /-- The recipients of the message. -/
-  recipients : List ObjectId
+  data : MessageData lab
+  /-- Signatures for `data`. -/
+  signatures : List Signature
 
 def Message.rawSignatures {lab : Ecosystem.Label} (msg : Message lab) : List Nat :=
-  let {id := id, signatures := signatures, ..} := msg
-  match id with
-  | .multiMethodId m => lab.MultiMethodSignatureIdEnum m |>.toList.map (fun s => signatures s |>.raw)
-  | .classMember (classId := clab) c => match c with
-    | .methodId m => clab.label.MethodSignatureIdEnum m |>.toList.map (fun s => signatures s |>.raw)
-    | .destructorId m => clab.label.DestructorSignatureIdEnum m |>.toList.map (fun s => signatures s |>.raw)
-    | .constructorId m => clab.label.ConstructorSignatureIdEnum m |>.toList.map (fun s => signatures s |>.raw)
-    | .upgradeId => []
+  msg.signatures.map Signature.raw
 
 instance Message.instHashable (lab : Ecosystem.Label) : Hashable (Message lab) where
   hash m := Hashable.Mix.run do
-    mix m.id
+    mix m.data.id
 
 instance Message.hasTypeRep (lab : Ecosystem.Label) : TypeRep (Message lab) where
   rep := Rep.composite "AVM.Message" [Rep.atomic lab.name]
 
 instance Message.hasBEq {lab : Ecosystem.Label} : BEq (Message lab) where
   beq a b :=
-    let {id := aid, args := aargs, signatures := asigs, ..} := a
-    let {id := bid, args := bargs, signatures := bsigs, ..} := b
-    check h : aid == bid
-    let h' := eq_of_beq h
-    check a.vals === b.vals
-    check s : aargs == cast (by simp! [h']) bargs
-    check a.recipients == b.recipients
-    check a.rawSignatures == b.rawSignatures
+    a.data == b.data && a.rawSignatures == b.rawSignatures
 
 structure SomeMessage : Type 1 where
   {label : Ecosystem.Label}
@@ -68,13 +41,13 @@ instance SomeMessage.hasBEq : BEq SomeMessage where
 instance : Inhabited SomeMessage where
   default := { label := Ecosystem.Label.dummy
                message :=
-                { id := .classMember (classId := .unit) (.constructorId PUnit.unit)
-                  Vals := ⟨PUnit⟩
-                  vals := PUnit.unit
-                  logicRef := default
-                  signatures f := nomatch f
-                  args := PUnit.unit
-                  recipients := [] }}
+                { data :=
+                    { id := .classMember (classId := .unit) (.constructorId PUnit.unit)
+                      Vals := ⟨PUnit⟩
+                      vals := PUnit.unit
+                      args := PUnit.unit
+                      recipients := [] },
+                  signatures := [] }}
 
 def Message.toSomeMessage {lab : Ecosystem.Label} (msg : Message lab) : SomeMessage :=
   { label := lab, message := msg }
diff --git a/AVM/Message/Data.lean b/AVM/Message/Data.lean
new file mode 100644
index 00000000..b2f38c83
--- /dev/null
+++ b/AVM/Message/Data.lean
@@ -0,0 +1,32 @@
+import AVM.Ecosystem.Data
+
+namespace AVM
+
+/-- A message is a communication sent from one object to another in the AVM. -/
+structure MessageData (lab : Ecosystem.Label) : Type 1 where
+  /-- The message ID. -/
+  id : lab.MemberId
+  {Vals : SomeType.{0}}
+  /-- Message parameter values. The message parameters are object resources and
+    generated random values that are used in the body of the call associated with
+    the message. These need to be provided in the message, because the
+    associated Resource Logic cannot fetch object resources from the Anoma
+    system or generate new object identifiers. -/
+  vals : Vals.type
+  /-- The arguments of the message. -/
+  args : id.Args.type
+  /-- The recipients of the message. -/
+  recipients : List ObjectId
+
+instance MessageData.hasTypeRep (lab : Ecosystem.Label) : TypeRep (MessageData lab) where
+  rep := Rep.composite "AVM.MessageData" [Rep.atomic lab.name]
+
+instance MessageData.hasBEq {lab : Ecosystem.Label} : BEq (MessageData lab) where
+  beq a b :=
+    let {id := aid, args := aargs, ..} := a
+    let {id := bid, args := bargs, ..} := b
+    check h : aid == bid
+    let h' := eq_of_beq h
+    check a.vals === b.vals
+    check s : aargs == cast (by simp! [h']) bargs
+    check a.recipients == b.recipients
diff --git a/AVM/Program.lean b/AVM/Program.lean
index 670e3f86..7fcf8f9e 100644
--- a/AVM/Program.lean
+++ b/AVM/Program.lean
@@ -14,7 +14,7 @@ inductive Program.{u} (scope : Scope.Label) (ReturnType : Type u) : Type (max u
     (cid : eid.label.ClassId)
     (constrId : cid.label.ConstructorId)
     (args : constrId.Args.type)
-    (signatures : constrId.Signatures args)
+    (signatures : MessageData eid.label → List Signature)
     (next : ObjectId → Program scope ReturnType)
     : Program scope ReturnType
   | /-- Destructor call. -/
@@ -24,7 +24,7 @@ inductive Program.{u} (scope : Scope.Label) (ReturnType : Type u) : Type (max u
     (destrId : cid.label.DestructorId)
     (selfId : ObjectId)
     (args : destrId.Args.type)
-    (signatures : destrId.Signatures args)
+    (signatures : MessageData eid.label → List Signature)
     (next : Program scope ReturnType)
     : Program scope ReturnType
   | /-- Method call. -/
@@ -34,7 +34,7 @@ inductive Program.{u} (scope : Scope.Label) (ReturnType : Type u) : Type (max u
     (methodId : cid.label.MethodId)
     (selfId : ObjectId)
     (args : methodId.Args.type)
-    (signatures : methodId.Signatures args)
+    (signatures : MessageData eid.label → List Signature)
     (next : Program scope ReturnType)
     : Program scope ReturnType
   | /-- MultiMethod call. -/
@@ -43,7 +43,7 @@ inductive Program.{u} (scope : Scope.Label) (ReturnType : Type u) : Type (max u
     (mid : eid.label.MultiMethodId)
     (selvesIds : mid.SelvesIds)
     (args : mid.Args.type)
-    (signatures : mid.Signatures args)
+    (signatures : MessageData eid.label → List Signature)
     (next : Program scope ReturnType)
     : Program scope ReturnType
   | /-- Object upgrade -/
diff --git a/Applib/Surface/Member.lean b/Applib/Surface/Member.lean
index 2fe7248d..a6080854 100644
--- a/Applib/Surface/Member.lean
+++ b/Applib/Surface/Member.lean
@@ -10,17 +10,16 @@ macro "noDestructors" : term => `(fun x => Empty.elim x)
 macro "noMethods" : term => `(fun x => Empty.elim x)
 
 def unsigned
-  {Args SignatureId : Type}
-  {args : Args}
-  : SignatureId → Signature args := fun _ => Signature.sign args PrivateKey.universal
+  {lab : Ecosystem.Label}
+  : MessageData lab → List Signature := fun _ => []
 
 def defMethod (cl : Type) [i : IsObject cl] {methodId : i.classId.label.MethodId}
  (body : (self : cl) → methodId.Args.type → Program i.label.toScope cl)
- (invariant : (self : cl) → (args : methodId.Args.type) → methodId.Signatures args → Bool := fun _ _ _ => true)
+ (invariant : (msg : Message i.label) → (self : cl) → (args : methodId.Args.type) → Bool := fun _ _ _ => true)
  : Class.Method i.classId methodId where
-    invariant (self : Object i.classId) (args : methodId.Args.type) :=
+    invariant (msg : Message i.label) (self : Object i.classId) (args : methodId.Args.type) :=
       let self' : cl := i.fromObject self.data
-      invariant self' args
+      invariant msg self' args
     body (self : Object i.classId) (args : methodId.Args.type) :=
       let self' := i.fromObject self.data
       let prog := body self' args
@@ -29,17 +28,17 @@ def defMethod (cl : Type) [i : IsObject cl] {methodId : i.classId.label.MethodId
 
 def defConstructor {cl : Type} [i : IsObject cl] {constrId : i.classId.label.ConstructorId}
  (body : constrId.Args.type → Program i.label.toScope cl)
- (invariant : (args : constrId.Args.type) → (signatures : constrId.Signatures args) → Bool := fun _ _ => true)
+ (invariant : (msg : Message i.label) → (args : constrId.Args.type) → Bool := fun _ _ => true)
  : Class.Constructor i.classId constrId where
-    invariant (args : constrId.Args.type) := invariant args
+    invariant (msg : Message i.label) (args : constrId.Args.type) := invariant msg args
     body (args : constrId.Args.type) := body args |>.map i.toObject |>.toAVM
 
 def defDestructor {cl : Type} [i : IsObject cl] {destructorId : i.classId.label.DestructorId}
  (body : (self : cl) → destructorId.Args.type → Program i.label.toScope PUnit := fun _ _ => Program.return ())
- (invariant : (self : cl) -> (args : destructorId.Args.type) → destructorId.Signatures args → Bool := fun _ _ _ => true)
+ (invariant : (msg : Message i.label) → (self : cl) -> (args : destructorId.Args.type) → Bool := fun _ _ _ => true)
  : Class.Destructor i.classId destructorId where
-    invariant (self : Object i.classId) (args : destructorId.Args.type) (signatures : destructorId.Signatures args) :=
+    invariant (msg : Message i.label) (self : Object i.classId) (args : destructorId.Args.type) :=
       let self' := i.fromObject self.data
-      invariant self' args signatures
+      invariant msg self' args
     body (self : Object i.classId) (args : destructorId.Args.type) :=
       body (i.fromObject self.data) args |>.toAVM
diff --git a/Applib/Surface/MultiMethod.lean b/Applib/Surface/MultiMethod.lean
index a3f083fa..a65479a6 100644
--- a/Applib/Surface/MultiMethod.lean
+++ b/Applib/Surface/MultiMethod.lean
@@ -59,12 +59,12 @@ def defMultiMethod
   (multiId : lab.MultiMethodId)
   (argsInfo : (a : multiId.ObjectArgNames) → ObjectArgInfo lab multiId a)
   (body : ObjectArgs lab multiId argsInfo → multiId.Args.type → Program lab.toScope (MultiMethodResult multiId))
-  (invariant : ObjectArgs lab multiId argsInfo → (args : multiId.Args.type) → (signatures : multiId.Signatures args) → Bool := fun _ _ _ => true)
+  (invariant : AVM.Message lab → ObjectArgs lab multiId argsInfo → (args : multiId.Args.type) → Bool := fun _ _ _ => true)
   : AVM.Ecosystem.MultiMethod multiId where
   body (selves : multiId.Selves) (args : multiId.Args.type) : AVM.Program lab.toScope (AVM.MultiMethodResult multiId) :=
     (body (getArg selves) args).map (MultiMethodResult.toAVM) |>.toAVM
-  invariant (selves : multiId.Selves) (args : multiId.Args.type) (signatures : multiId.Signatures args) : Bool :=
-    invariant (getArg selves) args signatures
+  invariant (msg : AVM.Message lab) (selves : multiId.Selves) (args : multiId.Args.type) : Bool :=
+    invariant msg (getArg selves) args
   where
     getArg (selves : multiId.Selves) (argName : multiId.ObjectArgNames) : (argsInfo argName).type :=
       (argsInfo argName).isObjectOf.fromObject (selves argName).data
diff --git a/Applib/Surface/Program.lean b/Applib/Surface/Program.lean
index bb392993..69193038 100644
--- a/Applib/Surface/Program.lean
+++ b/Applib/Surface/Program.lean
@@ -13,7 +13,7 @@ inductive Program (lab : Scope.Label) : (α : Type u) → Type (u + 1) where
     (cid : eid.label.ClassId)
     (constrId : cid.label.ConstructorId)
     (args : constrId.Args.type)
-    (signatures : constrId.Signatures args)
+    (signatures : MessageData eid.label → List Signature)
     (next : ObjectId → Program lab α)
     : Program lab α
   | destroy
@@ -23,7 +23,7 @@ inductive Program (lab : Scope.Label) : (α : Type u) → Type (u + 1) where
     (destrId : cid.label.DestructorId)
     (selfId : ObjectId)
     (args : destrId.Args.type)
-    (signatures : destrId.Signatures args)
+    (signatures : MessageData eid.label → List Signature)
     (next : Program lab α)
     : Program lab α
   | call
@@ -33,7 +33,7 @@ inductive Program (lab : Scope.Label) : (α : Type u) → Type (u + 1) where
     (methodId : cid.label.MethodId)
     (selfId : ObjectId)
     (args : methodId.Args.type)
-    (signatures : methodId.Signatures args)
+    (signatures : MessageData eid.label → List Signature)
     (next : Program lab α)
     : Program lab α
   | multiCall
@@ -42,7 +42,7 @@ inductive Program (lab : Scope.Label) : (α : Type u) → Type (u + 1) where
     (multiId : eid.label.MultiMethodId)
     (selves : multiId.SelvesIds)
     (args : multiId.Args.type)
-    (signatures : multiId.Signatures args)
+    (signatures : MessageData eid.label → List Signature)
     (next : Program lab α)
     : Program lab α
   | upgrade
@@ -125,7 +125,7 @@ def Program.create'
   (inScope : i.label ∈ lab)
   (constrId : i.classId.label.ConstructorId)
   (args : constrId.Args.type)
-  (signatures : constrId.Signatures args)
+  (signatures : MessageData i.label → List Signature)
   (next : Reference C → Program lab α)
   : Program lab α :=
   let ⟨eid, _⟩ := inScope
@@ -146,7 +146,7 @@ def Program.destroy'
   (inScope : i.label ∈ lab)
   (destrId : i.classId.label.DestructorId)
   (args : destrId.Args.type)
-  (signatures : destrId.Signatures args)
+  (signatures : MessageData i.label → List Signature)
   (next : Program lab α)
   : Program lab α :=
   let ⟨eid, _⟩ := inScope
@@ -168,7 +168,7 @@ def Program.call'
   (inScope : i.label ∈ lab)
   (methodId : i.classId.label.MethodId)
   (args : methodId.Args.type)
-  (signatures : methodId.Signatures args)
+  (signatures : MessageData i.label → List Signature)
   (next : Program lab α)
   : Program lab α :=
   let ⟨eid, _⟩ := inScope
@@ -203,7 +203,7 @@ def Program.multiCall'
   (multiId : eid.label.MultiMethodId)
   (selves : multiId.SelvesReferences)
   (args : multiId.Args.type)
-  (signatures : multiId.Signatures args)
+  (signatures : MessageData eid.label → List Signature)
   (next : Program lab α)
   : Program lab α :=
   let selves' : multiId.SelvesIds := fun x => selves x |>.ref.objId
diff --git a/Apps/Kudos.lean b/Apps/Kudos.lean
index 7b4730c0..000a5c85 100644
--- a/Apps/Kudos.lean
+++ b/Apps/Kudos.lean
@@ -14,8 +14,8 @@ open Applib
 /- 3. Burn: The owner of a kudos token can destroy it if themself is the originator of the token -/
 
 structure KudosData where
-  originator : PublicKey
-  owner : PublicKey
+  originator : AVM.PublicKey
+  owner : AVM.PublicKey
   deriving DecidableEq, Inhabited, Hashable
 
 structure Kudos extends KudosData where
@@ -104,17 +104,14 @@ def clab : Class.Label where
   MethodId := Methods
   MethodArgs := fun
     | Methods.Transfer => ⟨TransferArgs⟩
-  MethodSignatureId := Methods.SignatureId
 
   ConstructorId := Constructors
   ConstructorArgs := fun
     | Constructors.Mint => ⟨MintArgs⟩
-  ConstructorSignatureId := Constructors.SignatureId
 
   DestructorId := Destructors
   DestructorArgs := fun
     | Destructors.Burn => ⟨PUnit⟩
-  DestructorSignatureId := Destructors.SignatureId
 
 inductive MultiMethods where
   | Merge
@@ -199,17 +196,17 @@ def kudosMint : @Class.Constructor label .unit Constructors.Mint := defConstruct
         owner := args.originator
         originator := args.originator : Kudos}
   ⟫)
-  (invariant := fun (args : MintArgs) signatures => checkSignature (signatures .originator) args.originator)
+  (invariant := fun msg (args : MintArgs) => msg.checkSignature args.originator)
 
 def kudosTransfer : @Class.Method label .unit Methods.Transfer := defMethod Kudos
   (body := fun (self : Kudos) (args : TransferArgs) =>
     ⟪return {self with owner := args.newOwner : Kudos}⟫)
-  (invariant := fun (self : Kudos) (_args : TransferArgs) signatures =>
-    checkSignature (signatures .owner) self.owner)
+  (invariant := fun msg (self : Kudos) (_args : TransferArgs) =>
+    msg.checkSignature self.owner)
 
 def kudosBurn : @Class.Destructor label .unit Destructors.Burn := defDestructor
-  (invariant := fun (self : Kudos) (_args : PUnit) signatures =>
-    checkSignature (signatures .owner) self.owner
+  (invariant := fun msg (self : Kudos) (_args : PUnit) =>
+    msg.checkSignature self.owner
     && self.originator == self.owner)
 
 def kudosClass : @Class label .unit where
@@ -243,10 +240,11 @@ def kudosEcosystem : Ecosystem label where
                     }
                   }
                 ⟫)
-        (invariant := fun kudos _args _signatures =>
+        (invariant := fun msg kudos _args =>
                   let k1 := kudos .Kudos1
                   let k2 := kudos .Kudos2
-                  k1.originator == k2.originator
+                  msg.checkSignature k1.owner
+                  && k1.originator == k2.originator
                   && k1.owner == k2.owner)
 
     | .Split =>
diff --git a/Apps/KudosBank.lean b/Apps/KudosBank.lean
index 6db9d41a..4af2545e 100644
--- a/Apps/KudosBank.lean
+++ b/Apps/KudosBank.lean
@@ -2,6 +2,7 @@ import AVM
 import Applib
 
 open Applib
+open AVM
 
 def Std.HashMap.modifyDefault
 {α : Type u} {β : Type v} [BEq α] [Hashable α] [Inhabited β] (m : HashMap α β) (a : α) (f : β → β) : HashMap α β := m.alter a fun
@@ -249,7 +250,6 @@ def BankLabel : Class.Label where
     | Methods.Transfer => ⟨TransferArgs⟩
     | Methods.Mint => ⟨MintArgs⟩
     | Methods.Burn => ⟨BurnArgs⟩
-  MethodSignatureId := Methods.SignatureId
 
   ConstructorId := Constructors
   ConstructorArgs := fun
@@ -258,7 +258,6 @@ def BankLabel : Class.Label where
   DestructorId := Destructors
   DestructorArgs := fun
     | Destructors.Close => ⟨PUnit⟩
-  DestructorSignatureId := Destructors.SignatureId
 
 inductive MultiMethods where
   | IssueCheck
@@ -404,12 +403,6 @@ def label : AVM.Ecosystem.Label where
      | .auction => Classes.Auction
    | MultiMethods.EndAuction => fun
      | .auction => Classes.Auction
-  MultiMethodSignatureId := fun
-    | .IssueCheck => IssueCheck.SignatureId
-    | .DepositCheck => DepositCheck.SignatureId
-    | .NewAuction => NewAuction.SignatureId
-    | .Bid => Bid.SignatureId
-    | .EndAuction => EndAuction.SignatureId
   ObjectArgNamesBEq (f : MultiMethods) := by cases f <;> exact inferInstance
   ObjectArgNamesEnum (f : MultiMethods) := by cases f <;> exact inferInstance
 
@@ -471,9 +464,9 @@ def kudosTransfer : @Class.Method label Classes.Bank Methods.Transfer := defMeth
         |> Balances.addTokens args.newOwner args.denom args.quantity
         |> Balances.subTokens args.oldOwner args.denom args.quantity)
   ⟫)
-  (invariant := fun (self : KudosBank) (args : TransferArgs) signatures =>
+  (invariant := fun (msg : Message label) (self : KudosBank) (args : TransferArgs) =>
     0 < args.quantity
-    && checkSignature (signatures .owner) args.oldOwner
+    && msg.checkSignature args.oldOwner
     && args.quantity <= self.getBalance args.oldOwner args.denom)
 
 def kudosBurn : @Class.Method label Classes.Bank Methods.Burn := defMethod KudosBank
@@ -482,15 +475,15 @@ def kudosBurn : @Class.Method label Classes.Bank Methods.Burn := defMethod Kudos
       self.overBalances (fun b => b
         |> Balances.subTokens args.denom.originator args.denom args.quantity)
   ⟫)
-  (invariant := fun (self : KudosBank) (args : BurnArgs) signatures =>
-    checkSignature (signatures .originator) args.denom.originator
-    && checkSignature (signatures .owner) args.owner
+  (invariant := fun (msg : Message label) (self : KudosBank) (args : BurnArgs) =>
+    msg.checkSignature args.denom.originator
+    && msg.checkSignature args.owner
     && 0 < args.quantity
     && args.quantity <= self.getBalance args.denom.originator args.denom)
 
 def kudosClose : @Class.Destructor label Classes.Bank Destructors.Close := defDestructor
-  (invariant := fun (self : KudosBank) (_args : PUnit) signatures =>
-    checkSignature (signatures .owner) self.owner
+  (invariant := fun (msg : Message label) (self : KudosBank) (_args : PUnit) =>
+    msg.checkSignature self.owner
     && self.balances.isEmpty)
 
 def kudosClass : @Class label Classes.Bank where
@@ -543,9 +536,9 @@ def issueCheck : @Ecosystem.MultiMethod label .IssueCheck :=
                           quantity := args.quantity
                           : Check }]}
     ⟫)
-  (invariant := fun selves args signatures =>
+  (invariant := fun msg selves args =>
     let bank := selves .bank
-    checkSignature (signatures .owner) args.owner
+    msg.checkSignature args.owner
     && 0 < args.quantity
     && args.quantity <= bank.getBalance args.owner args.denomination)
 
@@ -571,8 +564,8 @@ def depositCheck : @Ecosystem.MultiMethod label .DepositCheck :=
           | .bank => .Disassembled
           | .check => .Destroyed }
     ⟫)
-  (invariant := fun selves _args signatures =>
-    checkSignature (signatures .owner) (selves .check).owner)
+  (invariant := fun msg selves _args =>
+    msg.checkSignature (selves .check).owner)
 
 def newAuction : @Ecosystem.MultiMethod label .NewAuction :=
   defMultiMethod label .NewAuction
@@ -595,8 +588,8 @@ def newAuction : @Ecosystem.MultiMethod label .NewAuction :=
           match arg with
           | .check => .Destroyed }
     ⟫)
-  (invariant := fun selves _args signatures =>
-    checkSignature (signatures .owner) (selves .check).owner)
+  (invariant := fun msg selves _args =>
+    msg.checkSignature (selves .check).owner)
 
 def bid : @Ecosystem.MultiMethod label .Bid :=
   defMultiMethod label .Bid
@@ -631,10 +624,10 @@ def bid : @Ecosystem.MultiMethod label .Bid :=
           | .check => .Destroyed
           | .auction => .Disassembled }
     ⟫)
-  (invariant := fun selves _args signatures =>
+  (invariant := fun msg selves _args =>
     let bid := selves .check
     let auction := selves .auction
-    checkSignature (signatures .owner) bid.owner
+    msg.checkSignature bid.owner
     && bid.denomination == auction.biddingDenomination
     && bid.quantity > auction.highestBid)
 
@@ -662,9 +655,9 @@ def endAuction : @Ecosystem.MultiMethod label .EndAuction :=
           match arg with
           | .auction => .Destroyed }
     ⟫)
-  (invariant := fun selves _args signatures =>
+  (invariant := fun msg selves _args =>
     let auction := selves .auction
-    checkSignature (signatures .owner) auction.owner)
+    msg.checkSignature auction.owner)
 
 def kudosEcosystem : Ecosystem label where
   classes := fun
diff --git a/Apps/OwnedCounter.lean b/Apps/OwnedCounter.lean
index edbfe861..200b8f30 100644
--- a/Apps/OwnedCounter.lean
+++ b/Apps/OwnedCounter.lean
@@ -5,7 +5,7 @@ open Applib
 
 structure OwnedCounter where
   count : Nat
-  owner : PublicKey
+  owner : AVM.PublicKey
   deriving Inhabited, Repr, BEq, Hashable
 
 namespace OwnedCounter
@@ -62,12 +62,10 @@ def clab : Class.Label where
   MethodArgs := fun
     | Methods.Incr => ⟨Nat⟩
     | Methods.Transfer => ⟨PublicKey⟩
-  MethodSignatureId := Methods.SignatureId
   ConstructorId := Constructors
   ConstructorArgs := fun
     | Constructors.Zero => ⟨Unit⟩
   DestructorId := Destructors
-  DestructorSignatureId := Destructors.SignatureId
 
 def label : Ecosystem.Label := Ecosystem.Label.singleton clab
 
@@ -97,19 +95,19 @@ def counterConstructor : @Class.Constructor label .unit Constructors.Zero := def
 
 def counterIncr : @Class.Method label .unit Methods.Incr := defMethod OwnedCounter
   (body := fun (self : OwnedCounter) (step : Nat) => ⟪return self.incrementBy step⟫)
-  (invariant := fun (self : OwnedCounter) (_step : Nat) signatures =>
-    checkSignature (signatures .owner) self.owner)
+  (invariant := fun (msg : Message label) (self : OwnedCounter) (_step : Nat) =>
+    msg.checkSignature self.owner)
 
 def counterTransfer : @Class.Method label .unit Methods.Transfer := defMethod OwnedCounter
   (body := fun (self : OwnedCounter) (newOwner : PublicKey) =>
     ⟪return {self with owner := newOwner : OwnedCounter}⟫)
-  (invariant := fun (self : OwnedCounter) (_newOwner : PublicKey) signatures =>
-    checkSignature (signatures .owner) self.owner)
+  (invariant := fun msg (self : OwnedCounter) (_newOwner : PublicKey) =>
+    msg.checkSignature self.owner)
 
 /-- We only allow the counter to be destroyed if its count is at least 10 -/
 def counterDestroy : @Class.Destructor label .unit Destructors.Ten := defDestructor
-  (invariant := fun (self : OwnedCounter) () signatures =>
-    checkSignature (signatures .owner) self.owner
+  (invariant := fun (msg : Message label) (self : OwnedCounter) () =>
+    msg.checkSignature self.owner
     && self.count >= 10)
 
 def counterClass : @Class label .unit where
diff --git a/SUMMARY.md b/SUMMARY.md
index 4751497f..00ec1366 100644
--- a/SUMMARY.md
+++ b/SUMMARY.md
@@ -19,6 +19,7 @@ A high-level summary description of GOOSE v0.3.1. The description intentionally
 		- [MultiMethod](#multimethod)
 		- [Class](#class)
 		- [Ecosystem](#ecosystem)
+		- [Authorization](#authorization)
 	- [AVM -\> RM translation](#avm---rm-translation)
 		- [Object](#object-1)
 			- [Resource data check](#resource-data-check)
@@ -204,11 +205,10 @@ Action sending the call messages:
   - `vals : Vals`. Message parameter values. The message parameters are object resources and generated random values that are used in the body of the call associated with the message. These need to be provided in the message, because the associated Resource Logic cannot fetch object resources from the Anoma system or generate new object identifiers.
   - `id : MessageId`. The message ID.
   - `args : id.Args`. The arguments of the message, where `id.Args` is the type of arguments based on the message id. The message arguments are the non-self arguments of the corresponding member or multi-method call.
-  - `data : Option MultiMethodData`. Extra data for multi-methods which contains the numbers of:
-    - disassembled selves,
-    - destroyed selves,
-    - constructed objects.
   - `recipients : List ObjectId`. The recipients of the message.
+  - `signatures : List Signature`. Authorization signatures for the message. Each signature consists of:
+    - public identifier of the signer,
+    - signature data: the message `id`, `args` and `vals` cryptographically signed with signer's private key.
 
 ### Constructor
 - `Class.Constructor` in `AVM/Class/Member.lean`
@@ -218,7 +218,7 @@ Action sending the call messages:
 	- `id : label.ConstructorId` determines the unique id of the constructor.
 	- `Args := label.ConstructorArgs id` is the type of constructor arguments.
 	- `body : Args -> Program ObjectData`. Constructor body, returning the object data for the object created by the constructor call.
-	- `invariant : Args -> Bool`. Extra constructor logic. The constructor message logic is a conjunction of auto-generated constructor logic and the extra constructor logic.
+	- `invariant : Message -> Args -> Bool`. Extra constructor logic. The constructor message logic is a conjunction of auto-generated constructor logic and the extra constructor logic.
 
 ### Destructor
 - `Class.Destructor` in `AVM/Class/Member.lean`
@@ -228,7 +228,7 @@ Action sending the call messages:
 	- `id : label.DestructorId` determines the unique id of the destructor.
 	- `Args := label.DestructorArgs id` is the type of destructor arguments excluding `self`.
 	- `body : (self : Object) -> Args -> Program Unit`. Destructor body program.
-	- `invariant : (self : Object) -> Args -> Bool`. Extra destructor logic. The destructor message logic is a conjunction of auto-generated destructor logic and the extra destructor logic.
+	- `invariant : Message -> (self : Object) -> Args -> Bool`. Extra destructor logic. The destructor message logic is a conjunction of auto-generated destructor logic and the extra destructor logic.
 
 ### Method
 - `Class.Method` in `AVM/Class/Member.lean`
@@ -238,7 +238,7 @@ Action sending the call messages:
 	- `id : label.MethodId` determines the unique id of the method.
 	- `Args := label.MethodArgs id` is the type of method arguments excluding `self`.
 	- `body : (self : Object) -> Args -> Program Object`. Method body program. The return value is the updated `self`.
-	- `invariant : (self : Object) -> Args -> Bool`. Extra method logic. The method message logic is a conjunction of auto-generated method logic and the extra method logic.
+	- `invariant : Message -> (self : Object) -> Args -> Bool`. Extra method logic. The method message logic is a conjunction of auto-generated method logic and the extra method logic.
 
 ### MultiMethod
 - `MultiMethod` in `AVM/Ecosystem/Member.lean`
@@ -253,7 +253,7 @@ Action sending the call messages:
 		- `destroyed : List Object`. List of destroyed selves. Destroyed object resources are balanced with automatically generated created ephemeral resources. The `destroyed` list must be a sublist of `selves`.
 		- `assembled : List Object`. List of assembled objects into which disassembled objects are transformed as a result of the multi-method call. It is the responsibility of the user to ensure that assembled object resources balance with the disassembled selves.
 		- `constructed : List Object`. List of constructed objects. Constructed object resources are balanced with automatically generated consumed ephemeral resources.
-	- `invariant : (selves : List Object) -> Args -> Bool`. Extra multi-method logic. The multi-method message logic is a conjunction of the auto-generated multi-method logic and the extra multi-method logic.
+	- `invariant : Message -> (selves : List Object) -> Args -> Bool`. Extra multi-method logic. The multi-method message logic is a conjunction of the auto-generated multi-method logic and the extra multi-method logic.
 - `selves : List Object` in `body` and `invariant` above is a list of `self` arguments - objects whose classes are described by `label.MultiMethodSelves id`.
 - `selves = disassembled ++ destroyed`.
 
@@ -275,6 +275,11 @@ Action sending the call messages:
 	- `classes : Set Class`. Classes in the ecosystem. A class is in exactly one ecosystem.
 	- `multiMethods : Set MultiMethod`. Multi-methods in the ecosystem. A multi-method is in exactly one ecosystem.
 
+### Authorization
+The GOOSE framework provides a function `checkSignature : Message -> PublicKey -> Bool` which checks that a given message was signed with the private key corresponding to a given public key. In other words, `checkSignature(msg, pubKey)` checks that decrypting `msg.signature` with `pubKey` yields (a digest of) `msg`.
+
+The `checkSignature` function can be used in invariants to perform authorization of the received messages.
+
 ## AVM -> RM translation
 
 ### Object
@@ -594,12 +599,18 @@ Multi-method message logic has access to RL arguments which contain the followin
 
 - `consumed : List Resource`. List of resources consumed in the transaction.
 - `created : List Resource`. List of resources created in the transaction.
-- `msgRes : Resource`. The resource of the method message `msg`, which contains the method call arguments `args` and the `data` field with the numbers of:
+- `msgRes : Resource`. The resource of the method message `msg`, which contains the method call arguments `args` and parameter values `vals`.
+
+For a given multi-method, the number `n` of `selves` is specified in the
+multi-method definition. We re-create the `selves` objects from the first `n`
+object resources in `consumed`.
+
+With `selves`, `args` and `vals`, we compute the result of of the multi-method. In this way, we obtain the numbers of:
   - disassembled selves,
   - destroyed selves,
   - constructed objects.
 
-For a given multi-method, we use the numbers stored in `msg.data` to partition the object resources in `consumed` into:
+We use the above numbers to partition the object resources in `consumed` into:
 
 - `disassembledSelves` list of persistent object resources corresponding to disassembled selves,
 - `destroyedSelves` list of persistent object resources corresponding to destroyed selves,
diff --git a/Tests/Applib/Surface/Program/Syntax.lean b/Tests/Applib/Surface/Program/Syntax.lean
index 1a179ecb..1f264724 100644
--- a/Tests/Applib/Surface/Program/Syntax.lean
+++ b/Tests/Applib/Surface/Program/Syntax.lean
@@ -217,7 +217,7 @@ namespace OwnedCounter
 
 abbrev scope := label.toScope
 
-example (r : Reference OwnedCounter) (newOwner : PublicKey) : Program scope (Reference OwnedCounter) := ⟪
+example (r : Reference OwnedCounter) (newOwner : AVM.PublicKey) : Program scope (Reference OwnedCounter) := ⟪
   c := fetch r
   call OwnedCounter.Methods.Transfer r newOwner
   r' := create OwnedCounter OwnedCounter.Constructors.Zero ()