diff --git a/pkg/scrypto/scrypto_spec.gobra b/pkg/scrypto/scrypto_spec.gobra
index b33787ac5..c3fef85d4 100644
--- a/pkg/scrypto/scrypto_spec.gobra
+++ b/pkg/scrypto/scrypto_spec.gobra
@@ -19,8 +19,11 @@
 
 package scrypto
 
-import "hash"
-import sl "github.com/scionproto/scion/verification/utils/slices"
+import (
+    "hash"
+    sl "github.com/scionproto/scion/verification/utils/slices"
+    "github.com/scionproto/scion/verification/io"
+)
 
 // The error returned by initMac is produced deterministically depending on the key.
 // If an initial call to initmac succeeds with a key, then any subsequent
@@ -33,7 +36,9 @@ pure func ValidKeyForHash(key []byte) bool
 
 preserves acc(sl.Bytes(key, 0, len(key)), _)
 ensures   old(ValidKeyForHash(key)) ==> e == nil
-ensures   e == nil ==> (h != nil && h.Mem() && ValidKeyForHash(key))
+ensures   e == nil ==> (
+    h != nil && h.Mem() && ValidKeyForHash(key) &&
+    h === sh && sh.AsidMem() && sh.Asid() == asid)
 ensures   e != nil ==> e.ErrorMem()
 decreases _
-func InitMac(key []byte) (h hash.Hash, e error)
+func InitMac(key []byte, ghost asid io.AS) (h hash.Hash, ghost sh hash.ScionHashSpec, e error)
diff --git a/pkg/slayers/doc.go b/pkg/slayers/doc.go
index d27e24f6e..59c9844bb 100644
--- a/pkg/slayers/doc.go
+++ b/pkg/slayers/doc.go
@@ -63,7 +63,7 @@ even branching based on layer type... it'll handle an (scn, e2e, udp) or (scn, h
 
 Note: Great care has been taken to only lazily parse the SCION header, however, HBH and E2E
 extensions are currently eagerly parsed (if they exist). Thus, handling packets containing these
-extensions will be much slower (see the package benchmarks for reference).
+extensions will be much slower (see the Package benchmarks for reference).
 When using the DecodingLayerParser, the extensions can be explicitly skipped by using the
 HopByHop/EndToEndExtnSkipper layer. The content of this Skipper-layer can be decoded into the full
 representation when necessary.
diff --git a/pkg/slayers/path/io_msgterm_spec.gobra b/pkg/slayers/path/io_msgterm_spec.gobra
index 7331673bc..3e93a66be 100644
--- a/pkg/slayers/path/io_msgterm_spec.gobra
+++ b/pkg/slayers/path/io_msgterm_spec.gobra
@@ -48,7 +48,7 @@ pure func FromSliceToMacArray(mac []byte) (res [MacLen]byte) {
 }
 
 ghost
-requires len(mac1) == MacLen
+requires len(mac1) >= MacLen
 requires forall i int :: { &mac1[i] } 0 <= i && i < MacLen ==> acc(&mac1[i], R50)
 requires forall i int :: { &mac1[i] } 0 <= i && i < MacLen ==> mac1[i] == mac2[i]
 ensures  forall i int :: { &mac1[i] } 0 <= i && i < MacLen ==> acc(&mac1[i], R50)
diff --git a/pkg/slayers/path/mac.go b/pkg/slayers/path/mac.go
index df11254b7..1c8ef5637 100644
--- a/pkg/slayers/path/mac.go
+++ b/pkg/slayers/path/mac.go
@@ -19,8 +19,9 @@ package path
 import (
 	"encoding/binary"
 	"hash"
-	//@ . "github.com/scionproto/scion/verification/utils/definitions"
-	//@ sl "github.com/scionproto/scion/verification/utils/slices"
+	// @ . "github.com/scionproto/scion/verification/utils/definitions"
+	// @ sl "github.com/scionproto/scion/verification/utils/slices"
+	// @ io "verification/io"
 )
 
 const MACBufferSize = 16
@@ -29,15 +30,24 @@ const MACBufferSize = 16
 // https://docs.scion.org/en/latest/protocols/scion-header.html#hop-field-mac-computation
 // this method does not modify info or hf.
 // Modifying the provided buffer after calling this function may change the returned HopField MAC.
-// @ requires  h != nil && h.Mem()
+// @ requires  h != nil && h.Mem() && sh === h && acc(sh.AsidMem(), 1/2)
 // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer))
-// @ ensures   h.Mem()
+// @ ensures   h.Mem() && sh === h && acc(sh.AsidMem(), 1/2)
+// @ ensures   let absInf := info.ToAbsInfoField() in
+// @ 	let absHF := hf.Abs() in
+// @ 	let absMac := AbsMac(ret) in
+// @ 	absMac == io.nextMsgtermSpec(sh.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo)
 // @ decreases
-func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte) [MacLen]byte {
-	mac := FullMAC(h, info, hf, buffer)
-	var res /*@ @ @*/ [MacLen]byte
-	//@ unfold sl.Bytes(mac, 0, MACBufferSize)
+func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost sh hash.ScionHashSpec @*/) (ret [MacLen]byte) {
+	mac := FullMAC(h, info, hf, buffer /*@, sh @*/)
+	var res /*@@@*/ [MacLen]byte
+	// @ unfold sl.Bytes(mac, 0, MACBufferSize)
+
 	copy(res[:], mac[:MacLen] /*@, R1 @*/)
+
+	// @ assert forall i int :: { res[i] } 0 <= i && i < len(res[:]) ==> &res[:][i] == &res[i]
+	// @ EqualBytesImplyEqualMac(mac, res)
+
 	return res
 }
 
@@ -46,30 +56,44 @@ func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte) [MacLen]byte {
 // this method does not modify info or hf.
 // Modifying the provided buffer after calling this function may change the returned HopField MAC.
 // In contrast to MAC(), FullMAC returns all the 16 bytes instead of only 6 bytes of the MAC.
-// @ requires  h != nil && h.Mem()
+// @ requires  h != nil && h.Mem() && sh === h && acc(sh.AsidMem(), 1/2)
 // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer))
-// @ ensures   h.Mem()
+// @ ensures   h.Mem() && sh === h && acc(sh.AsidMem(), 1/2)
 // @ ensures   len(res) == MACBufferSize && sl.Bytes(res, 0, MACBufferSize)
+// @ ensures   unfolding sl.Bytes(res, 0, MACBufferSize) in
+// @ 	let absInf := info.ToAbsInfoField() in
+// @ 	let absHF := hf.Abs() in
+// @ 	let absMac := AbsMac(FromSliceToMacArray(res)) in
+// @ 	absMac == io.nextMsgtermSpec(sh.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo)
 // @ decreases
-func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte) (res []byte) {
+func FullMAC(h hash.Hash, info InfoField, hf HopField, buffer []byte /*@, ghost sh hash.ScionHashSpec @*/) (res []byte) {
 	if len(buffer) < MACBufferSize {
 		buffer = make([]byte, MACBufferSize)
-		//@ fold sl.Bytes(buffer, 0, len(buffer))
+		// @ fold sl.Bytes(buffer, 0, len(buffer))
 	}
 
 	h.Reset()
 	MACInput(info.SegID, info.Timestamp, hf.ExpTime,
 		hf.ConsIngress, hf.ConsEgress, buffer)
-	//@ unfold sl.Bytes(buffer, 0, len(buffer))
-	//@ defer fold sl.Bytes(buffer, 0, len(buffer))
+	// @ unfold sl.Bytes(buffer, 0, len(buffer))
+	// @ defer fold sl.Bytes(buffer, 0, len(buffer))
 	// Write must not return an error: https://godoc.org/hash#Hash
 	if _, err := h.Write(buffer); err != nil {
 		// @ Unreachable()
 		panic(err)
 	}
-	//@ assert h.Size() >= 16
+	// @ assert h.Size() >= 16
 	res = h.Sum(buffer[:0])[:16]
-	//@ fold sl.Bytes(res, 0, MACBufferSize)
+
+	// @ absInf := info.ToAbsInfoField()
+	// @ absHF := hf.Abs()
+	// @ absMac := AbsMac(FromSliceToMacArray(res))
+
+	// This is our "MAC assumption", linking the abstraction of the concrete MAC
+	// tag to the abstract computation of the MAC tag.
+	// @ AssumeForIO(absMac == io.nextMsgtermSpec(sh.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo))
+
+	// @ fold sl.Bytes(res, 0, MACBufferSize)
 	return res
 }
 
diff --git a/router/dataplane.go b/router/dataplane.go
index a2539743a..8557016b1 100644
--- a/router/dataplane.go
+++ b/router/dataplane.go
@@ -218,6 +218,7 @@ type DataPlane struct {
 	// (VerifiedSCION) This is stored in the dataplane in order to retain
 	// knowledge that macFactory will not fail.
 	// @ ghost key *[]byte
+	// @ ghost asid gpointer[io.AS]
 	external          map[uint16]BatchConn
 	linkTypes         map[uint16]topology.LinkType
 	neighborIAs       map[uint16]addr.IA
@@ -225,7 +226,7 @@ type DataPlane struct {
 	internalIP        net.IP
 	internalNextHops  map[uint16]*net.UDPAddr
 	svc               *services
-	macFactory        func() hash.Hash
+	macFactory        func() (hash.Hash /*@, ghost hash.ScionHashSpec @*/)
 	bfdSessions       map[uint16]bfdSession
 	localIA           addr.IA
 	mtx               sync.Mutex
@@ -274,6 +275,7 @@ func (e scmpError) Error() string {
 // @ requires  !d.IsRunning()
 // @ requires  d.LocalIA().IsZero()
 // @ requires  !ia.IsZero()
+// @ requires  !d.KeyIsSet()
 // @ preserves d.mtx.LockP()
 // @ preserves d.mtx.LockInv() == MutexInvariant!<d!>
 // @ ensures   acc(d.Mem(), OutMutexPerm)
@@ -342,22 +344,28 @@ func (d *DataPlane) SetKey(key []byte) (res error) {
 		// @ Unreachable()
 		return alreadySet
 	}
+
+	// @ ghost var asid@ io.AS = io.AS{uint(d.localIA)}
+
 	// First check for MAC creation errors.
-	if _, err := scrypto.InitMac(key); err != nil {
+	if _ /*@, macSpec @*/, err := scrypto.InitMac(key /*@, asid @*/); err != nil {
 		return err
 	}
 	// @ d.key = &key
+	// @ d.asid = &asid
 	verScionTemp :=
 		// @ requires acc(&key, _) && acc(sl.Bytes(key, 0, len(key)), _)
 		// @ requires scrypto.ValidKeyForHash(key)
+		// @ requires acc(&asid, _)
 		// @ ensures  acc(&key, _) && acc(sl.Bytes(key, 0, len(key)), _)
 		// @ ensures  h != nil && h.Mem()
+		// @ ensures  acc(&asid, _) && sh === h && sh.AsidMem() && sh.Asid() == asid
 		// @ decreases
-		func /*@ f @*/ () (h hash.Hash) {
-			mac, _ := scrypto.InitMac(key)
-			return mac
+		func /*@ f @*/ () (h hash.Hash /*@, ghost sh hash.ScionHashSpec @*/) {
+			mac /*@, macSpec @*/, _ := scrypto.InitMac(key /*@, asid @*/)
+			return mac /*@, macSpec @*/
 		}
-	// @ proof verScionTemp implements MacFactorySpec{d.key} {
+	// @ proof verScionTemp implements MacFactorySpec{d.key, d.asid} {
 	// @   return verScionTemp() as f
 	// @ }
 	d.macFactory = verScionTemp
@@ -764,7 +772,6 @@ func (d *DataPlane) AddNextHopBFD(ifID uint16, src, dst *net.UDPAddr, cfg contro
 			PacketsReceived: d.Metrics.SiblingBFDPacketsReceived.With(labels),
 		}
 	}
-
 	s := newBFDSend(d.internal, d.localIA, d.localIA, src, dst, 0, d.macFactory())
 	return d.addBFDController(ifID, s, cfg, m)
 }
@@ -921,6 +928,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 			// @ invariant d.getValForwardingMetrics() != nil
 			// @ invariant 0 elem d.getDomForwardingMetrics()
 			// @ invariant ingressID elem d.getDomForwardingMetrics()
+			// @ invariant d.KeyIsSet()
 			// @ invariant acc(rd.Mem(), _)
 			// @ invariant processor.sInit() && processor.sInitD() === d
 			// @ invariant let ubuf := processor.sInitBufferUBuf() in
@@ -993,6 +1001,7 @@ func (d *DataPlane) Run(ctx context.Context /*@, ghost place io.Place, ghost sta
 				// @ invariant d.getValForwardingMetrics() != nil
 				// @ invariant 0 elem d.getDomForwardingMetrics()
 				// @ invariant ingressID elem d.getDomForwardingMetrics()
+				// @ invariant d.KeyIsSet()
 				// @ invariant acc(rd.Mem(), _)
 				// @ invariant pkts <= len(msgs)
 				// @ invariant 0 <= i0 && i0 <= pkts
@@ -1438,16 +1447,18 @@ func newPacketProcessor(d *DataPlane, ingressID uint16) (res *scionPacketProcess
 	// @ d.getNewPacketProcessorFootprint()
 	verScionTmp = gopacket.NewSerializeBuffer()
 	// @ sl.PermsImplyIneqWithWildcard(verScionTmp.UBuf(), *d.key)
+	mac /*@, macSpec @*/ := (d.macFactory() /*@ as MacFactorySpec{d.key, d.asid} @*/)
 	p := &scionPacketProcessor{
 		d:         d,
 		ingressID: ingressID,
 		buffer:    verScionTmp,
-		mac:       (d.macFactory() /*@ as MacFactorySpec{d.key} @ */),
+		mac:       mac,
 		macBuffers: macBuffersT{
 			scionInput: make([]byte, path.MACBufferSize),
 			epicInput:  make([]byte, libepic.MACBufferSize),
 		},
 	}
+	// @ p.macSpec = macSpec
 	// @ fold sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput))
 	// @ fold slayers.PathPoolMem(p.scionLayer.pathPool, p.scionLayer.pathPoolRaw)
 	p.scionLayer.RecyclePaths()
@@ -1496,7 +1507,8 @@ func (p *scionPacketProcessor) reset() (err error) {
 // @ 	d.WellConfigured()        &&
 // @ 	d.getValSvc() != nil      &&
 // @ 	d.getValForwardingMetrics() != nil &&
-// @ 	d.DpAgreesWithSpec(dp)
+// @ 	d.DpAgreesWithSpec(dp)    &&
+// @ 	d.KeyIsSet()
 // @ requires let ubuf := p.sInitBufferUBuf() in
 // @ 	acc(sl.Bytes(ubuf, 0, len(ubuf)), writePerm)
 // @ ensures  p.sInit()
@@ -1638,7 +1650,8 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte,
 		// @ unfold acc(p.d.Mem(), _)
 		// @ assert reveal p.scionLayer.EqPathType(p.rawPkt)
 		// @ assert !(reveal slayers.IsSupportedPkt(p.rawPkt))
-		v1, v2 /*@, aliasesPkt, newAbsPkt @*/ := p.processOHP()
+		// @ reveal p.d.DpAgreesWithSpec(dp)
+		v1, v2 /*@, aliasesPkt, newAbsPkt @*/ := p.processOHP(/*@ dp @*/)
 		// @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, true, hasHbhLayer, hasE2eLayer)
 		// @ fold p.sInit()
 		return v1, v2 /*@, aliasesPkt, newAbsPkt @*/
@@ -1649,6 +1662,9 @@ func (p *scionPacketProcessor) processPkt(rawPkt []byte,
 		// @ 	sl.CombineRange_Bytes(p.rawPkt, o.start, o.end, HalfPerm)
 		// @ }
 		// @ assert sl.Bytes(p.rawPkt, 0, len(p.rawPkt))
+		// @ unfold acc(p.d.Mem(), _)
+		// @ reveal p.d.DpAgreesWithSpec(dp)
+		// @ assert p.d.dpSpecWellConfiguredLocalIA(dp)
 		v1, v2 /*@ , addrAliasesPkt, newAbsPkt @*/ := p.processSCION( /*@ p.rawPkt, ub == nil, llStart, llEnd, ioLock, ioSharedArg, dp @*/ )
 		// @ ResetDecodingLayers(&p.scionLayer, &p.hbhLayer, &p.e2eLayer, ubScionLayer, ubHbhLayer, ubE2eLayer, v2 == nil, hasHbhLayer, hasE2eLayer)
 		// @ fold p.sInit()
@@ -1798,6 +1814,8 @@ func (p *scionPacketProcessor) processIntraBFD(data []byte) (res error) {
 // @ preserves acc(&p.infoField)
 // @ preserves acc(&p.hopField)
 // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem()
+// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && 
+// @ 	p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid()
 // @ preserves acc(&p.macBuffers.scionInput, R10)
 // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput))
 // @ preserves acc(&p.cachedMac)
@@ -1920,6 +1938,9 @@ type scionPacketProcessor struct {
 	buffer gopacket.SerializeBuffer
 	// mac is the hasher for the MAC computation.
 	mac hash.Hash
+	// `macSpec` lets us access the AS identifier corresponding to the private
+	// key used by `mac`.
+	// @ ghost macSpec hash.ScionHashSpec
 
 	// scionLayer is the SCION gopacket layer.
 	scionLayer slayers.SCION
@@ -2857,6 +2878,8 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/
 // @ requires  acc(&p.infoField, R20)
 // @ requires  acc(&p.hopField, R20)
 // @ preserves acc(&p.mac, R20) && p.mac != nil && p.mac.Mem()
+// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec &&
+// @ 	p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid()
 // @ preserves acc(&p.macBuffers.scionInput, R20)
 // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput))
 // @ preserves acc(&p.cachedMac)
@@ -2897,12 +2920,11 @@ func (p *scionPacketProcessor) currentHopPointer( /*@ ghost ubScionL []byte @*/
 // @ decreases
 func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec, ghost ubScionL []byte, ghost ubLL []byte, ghost startLL int, ghost endLL int @*/ ) (respr processResult, reserr error) {
 	// @ ghost oldPkt := absPkt(ubScionL)
-	fullMac := path.FullMAC(p.mac, p.infoField, p.hopField, p.macBuffers.scionInput)
+	fullMac := path.FullMAC(p.mac, p.infoField, p.hopField, p.macBuffers.scionInput /*@, p.macSpec @*/)
 	// @ fold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21)
-	// @ defer unfold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21)
 	// @ sl.SplitRange_Bytes(fullMac, 0, path.MacLen, R21)
-	// @ ghost defer sl.CombineRange_Bytes(fullMac, 0, path.MacLen, R21)
 	if subtle.ConstantTimeCompare(p.hopField.Mac[:path.MacLen], fullMac[:path.MacLen]) == 0 {
+		// @ defer unfold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21)
 		// @ ghost ubPath := p.scionLayer.UBPath(ubScionL)
 		// @ ghost start := p.scionLayer.PathStartIdx(ubScionL)
 		// @ ghost end   := p.scionLayer.PathEndIdx(ubScionL)
@@ -2932,15 +2954,26 @@ func (p *scionPacketProcessor) verifyCurrentMAC( /*@ ghost dp io.DataPlaneSpec,
 		// @ }
 		return tmpRes, tmpErr
 	}
+
 	// Add the full MAC to the SCION packet processor,
 	// such that EPIC does not need to recalculate it.
 	p.cachedMac = fullMac
 	// @ reveal p.EqAbsInfoField(oldPkt)
 	// @ reveal p.EqAbsHopField(oldPkt)
-	// (VerifiedSCION) Assumptions for Cryptography:
-	// @ absInf := p.infoField.ToAbsInfoField()
+
 	// @ absHF := p.hopField.Abs()
-	// @ AssumeForIO(dp.hf_valid(absInf.ConsDir, absInf.AInfo.V, absInf.UInfo, absHF))
+	// @ absInf := p.infoField.ToAbsInfoField()
+
+	// @ assert forall i int :: { sl.GetByte(fullMac[:path.MacLen], 0, path.MacLen, i) } 0 <= i && i < path.MacLen ==>
+	// @ 	sl.GetByte(fullMac[:path.MacLen], 0, path.MacLen, i) ==
+	// @ 	unfolding acc(sl.Bytes(fullMac[:path.MacLen], 0, path.MacLen), R21) in fullMac[i]
+	// @ unfold acc(sl.Bytes(p.hopField.Mac[:path.MacLen], 0, path.MacLen), R21)
+	// @ unfold acc(sl.Bytes(fullMac[:path.MacLen], 0, path.MacLen), R21)
+	// @ path.EqualBytesImplyEqualMac(fullMac, p.hopField.Mac)
+
+	// @ unfold acc(sl.Bytes(fullMac, 0, len(fullMac)), R21)
+	// @ assert absHF.HVF == io.nextMsgtermSpec(dp.Asid(), absHF.InIF2, absHF.EgIF2, absInf.AInfo.V, absInf.UInfo)
+
 	// @ reveal AbsVerifyCurrentMACConstraint(oldPkt, dp)
 	// @ fold p.d.validResult(processResult{}, false)
 	return processResult{}, nil
@@ -3827,6 +3860,8 @@ func (p *scionPacketProcessor) validatePktLen( /*@ ghost ubScionL []byte, ghost
 // @ preserves acc(&p.infoField)
 // @ preserves acc(&p.hopField)
 // @ preserves acc(&p.mac, R10) && p.mac != nil && p.mac.Mem()
+// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && 
+// @ 	p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid()
 // @ preserves acc(&p.macBuffers.scionInput, R10)
 // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput))
 // @ preserves acc(&p.cachedMac)
@@ -4071,6 +4106,8 @@ func (p *scionPacketProcessor) process(
 // @ requires  sl.Bytes(p.rawPkt, 0, len(p.rawPkt))
 // @ preserves acc(&p.mac, R10)
 // @ preserves p.mac != nil && p.mac.Mem()
+// @ preserves acc(&p.macSpec, R20) && p.mac === p.macSpec && 
+// @ 	p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid()
 // @ preserves acc(&p.macBuffers.scionInput, R10)
 // @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput))
 // @ preserves acc(&p.buffer, R10) && p.buffer != nil && p.buffer.Mem()
@@ -4096,7 +4133,7 @@ func (p *scionPacketProcessor) process(
 // @ 	newAbsPkt == absIO_val(respr.OutPkt, respr.EgressID) &&
 // @ 	newAbsPkt.isValUnsupported
 // @ decreases 0 if sync.IgnoreBlockingForTermination()
-func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) {
+func (p *scionPacketProcessor) processOHP(/*@ ghost dp io.DataPlaneSpec @*/) (respr processResult, reserr error /*@ , ghost addrAliasesPkt bool, ghost newAbsPkt io.Val @*/) {
 	// @ ghost ubScionL := p.rawPkt
 	// @ p.scionLayer.ExtractAcc(ubScionL)
 	s := p.scionLayer
@@ -4155,10 +4192,12 @@ func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error /
 		// @ preserves acc(&ohp.Info, R55) && acc(&ohp.FirstHop, R55)
 		// @ preserves acc(&p.macBuffers.scionInput, R55)
 		// @ preserves acc(&p.mac, R55) && p.mac != nil && p.mac.Mem()
+		// @ preserves acc(&p.macSpec, R55) && p.mac === p.macSpec && 
+		// @ 	p.macSpec.AsidMem() && p.macSpec.Asid() == dp.Asid()
 		// @ preserves sl.Bytes(p.macBuffers.scionInput, 0, len(p.macBuffers.scionInput))
 		// @ decreases
 		// @ outline (
-		mac /*@@@*/ := path.MAC(p.mac, ohp.Info, ohp.FirstHop, p.macBuffers.scionInput)
+		mac /*@@@*/ := path.MAC(p.mac, ohp.Info, ohp.FirstHop, p.macBuffers.scionInput /*@, p.macSpec @*/)
 		// (VerifiedSCION) introduced separate copy to avoid exposing quantified permissions outside the scope of this outline block.
 		macCopy := mac
 		// @ fold acc(sl.Bytes(ohp.FirstHop.Mac[:], 0, len(ohp.FirstHop.Mac[:])), R56)
@@ -4235,7 +4274,7 @@ func (p *scionPacketProcessor) processOHP() (respr processResult, reserr error /
 	// XXX(roosd): Here we leak the buffer into the SCION packet header.
 	// This is okay because we do not operate on the buffer or the packet
 	// for the rest of processing.
-	ohp.SecondHop.Mac = path.MAC(p.mac, ohp.Info, ohp.SecondHop, p.macBuffers.scionInput)
+	ohp.SecondHop.Mac = path.MAC(p.mac, ohp.Info, ohp.SecondHop, p.macBuffers.scionInput /*@, p.macSpec @*/)
 	// @ fold ohp.SecondHop.Mem()
 	// @ fold s.Path.Mem(ubPath)
 	// @ fold acc(p.scionLayer.Mem(ubScionL), 1-R15)
diff --git a/router/dataplane_spec.gobra b/router/dataplane_spec.gobra
index ac0bc14a4..0769b38ae 100644
--- a/router/dataplane_spec.gobra
+++ b/router/dataplane_spec.gobra
@@ -32,6 +32,7 @@ import (
 
 	. "github.com/scionproto/scion/verification/utils/definitions"
 	sl "github.com/scionproto/scion/verification/utils/slices"
+	"github.com/scionproto/scion/verification/io"
 )
 
 ghost const MutexPerm perm = 1/4
@@ -59,6 +60,7 @@ pred (d *DataPlane) Mem() {
 	acc(&d.Metrics)                                               &&
 	acc(&d.forwardingMetrics)                                     &&
 	acc(&d.key)                                                   &&
+	acc(&d.asid)                                                  &&
 	(d.external    != nil       ==> accBatchConn(d.external))     &&
 	(d.linkTypes   != nil       ==> acc(d.linkTypes))             &&
 	(d.neighborIAs != nil       ==> acc(d.neighborIAs))           &&
@@ -67,11 +69,12 @@ pred (d *DataPlane) Mem() {
 	(d.internalNextHops != nil  ==> accAddr(d.internalNextHops))  &&
 	(d.svc != nil               ==> d.svc.Mem())                  &&
 	(d.macFactory != nil        ==> (
-		acc(d.key)                                      &&
-		acc(sl.Bytes(*d.key, 0, len(*d.key)), _)        &&
-		len(*d.key) > 0                                 &&
-		scrypto.ValidKeyForHash(*d.key)                 &&
-		d.macFactory implements MacFactorySpec{d.key}))           &&
+		acc(d.key)                                              &&
+		acc(sl.Bytes(*d.key, 0, len(*d.key)), _)                &&
+		len(*d.key) > 0                                         &&
+		scrypto.ValidKeyForHash(*d.key)                         &&
+		acc(d.asid) && *d.asid == io.AS{uint(d.localIA)}        &&
+		d.macFactory implements MacFactorySpec{d.key, d.asid})) &&
 	(d.bfdSessions != nil       ==> accBfdSession(d.bfdSessions)) &&
 	(d.Metrics != nil           ==> acc(d.Metrics.Mem(), _))      &&
 	// The following permissions are enough to call all methods needed in fields
@@ -149,10 +152,12 @@ pred (p *scionPacketProcessor) initMem() {
 // This is used as a signature, not as an assumed function.
 requires acc(key, _) && acc(sl.Bytes(*key, 0, len(*key)), _)
 requires scrypto.ValidKeyForHash(*key)
+requires acc(asid, _)
 ensures  acc(key, _) && acc(sl.Bytes(*key, 0, len(*key)), _)
-ensures  res != nil && res.Mem()
+ensures  h != nil && h.Mem() 
+ensures  acc(asid, _) && sh === h && sh.AsidMem() && sh.Asid() == *asid
 decreases
-func MacFactorySpec(ghost key *[]byte) (res hash.Hash)
+func MacFactorySpec(ghost key *[]byte, ghost asid gpointer[io.AS]) (h hash.Hash, ghost sh hash.ScionHashSpec)
 
 // useful to deal with incompletnesses
 pred hideLocalIA(p *addr.IA) {
@@ -218,7 +223,7 @@ pure func (p *scionPacketProcessor) getIngressID() uint16 {
 ghost
 requires d.Mem()
 decreases
-pure func (d *DataPlane) getMacFactory() func() hash.Hash {
+pure func (d *DataPlane) getMacFactory() func() (hash.Hash, ghost hash.ScionHashSpec) {
 	return unfolding d.Mem() in
 		d.macFactory
 }
@@ -419,7 +424,8 @@ ensures  acc(&d.macFactory, _) && acc(&d.key, _) && acc(d.key, _)
 ensures  acc(sl.Bytes(*d.key, 0, len(*d.key)), _)
 ensures  scrypto.ValidKeyForHash(*d.key)
 ensures  len(*d.key) > 0
-ensures  d.macFactory implements MacFactorySpec{d.key}
+ensures  acc(&d.asid, _) && acc(d.asid, _)
+ensures  d.macFactory implements MacFactorySpec{d.key, d.asid}
 decreases
 func (d *DataPlane) getNewPacketProcessorFootprint() {
 	unfold acc(d.Mem(), _)
@@ -565,6 +571,11 @@ pred (s* scionPacketProcessor) sInit() {
 	acc(&s.buffer) && s.buffer != nil            &&
 	s.buffer.Mem()                               &&
 	acc(&s.mac) && s.mac != nil && s.mac.Mem()   &&
+	acc(&s.macSpec)                              &&
+	acc(&s.d.asid, _) && acc(s.d.asid, _)        &&
+	s.mac === s.macSpec                          &&
+	s.macSpec.AsidMem()                          &&
+	s.macSpec.Asid() == *s.d.asid                &&
 	s.scionLayer.NonInitMem()                    &&
 	// The following is not necessary
 	// s.scionLayer.PathPoolInitializedNonInitMem() &&
diff --git a/router/dataplane_spec_test.gobra b/router/dataplane_spec_test.gobra
index 41e2e651d..bb0b374d0 100644
--- a/router/dataplane_spec_test.gobra
+++ b/router/dataplane_spec_test.gobra
@@ -85,12 +85,14 @@ requires macFactory != nil                        &&
 	len(*key) > 0                                 &&
 	acc(sl.Bytes(*key, 0, len(*key)), _)          &&
 	scrypto.ValidKeyForHash(*key)                 &&
-	macFactory implements MacFactorySpec{key}
+	acc(asid) && asid.V == 1000                   &&
+	macFactory implements MacFactorySpec{key, asid}
 requires metrics != nil && metrics.Mem()
 requires ctx != nil && ctx.Mem()
 func testRun(
-	macFactory func() hash.Hash,
+	macFactory func() (hash.Hash, ghost hash.ScionHashSpec),
 	key *[]byte,
+	ghost asid gpointer[io.AS],
 	metrics *Metrics,
 	ctx context.Context,
 	ghost place io.Place,
@@ -129,6 +131,7 @@ func testRun(
 	d.svc = newServices()
 	d.macFactory = macFactory
 	d.key = key
+	d.asid = asid
 	d.localIA = 1000
 	d.Metrics = metrics
 	d.bfdSessions = make(map[uint16]bfdSession)
diff --git a/router/io-spec-lemmas.gobra b/router/io-spec-lemmas.gobra
index 81ffb39d1..035a68caa 100644
--- a/router/io-spec-lemmas.gobra
+++ b/router/io-spec-lemmas.gobra
@@ -274,6 +274,7 @@ func (p* scionPacketProcessor) AbsPktToSubSliceAbsPkt(ub []byte, start int, end
 	assert reveal scion.validPktMetaHdr(ub[start:end])
 	unfold acc(p.scionLayer.Mem(ub), R56)
 	reveal p.scionLayer.ValidHeaderOffset(ub, len(ub))
+	assert p.path.GetBase(ub[start:end]) == scion.RawBytesToBase(ub[start:end])
 	assert p.path.GetBase(ub[start:end]).EqAbsHeader(ub[start:end])
 	fold acc(p.scionLayer.Mem(ub), R56)
 	assert start == slayers.GetAddressOffset(ub)
diff --git a/verification/dependencies/crypto/subtle/constant_time.gobra b/verification/dependencies/crypto/subtle/constant_time.gobra
index 68b411b07..e1330daf3 100644
--- a/verification/dependencies/crypto/subtle/constant_time.gobra
+++ b/verification/dependencies/crypto/subtle/constant_time.gobra
@@ -18,5 +18,8 @@ trusted
 requires sl.Bytes(x, 0, len(x))
 requires sl.Bytes(y, 0, len(y))
 ensures  len(x) != len(y) ==> res == 0
+ensures  res != 0 ==>
+    forall i int :: { sl.GetByte(x, 0, len(x), i) }{ sl.GetByte(y, 0, len(y), i) } 0 <= i && i < len(x) ==>
+        sl.GetByte(x, 0, len(x), i) == sl.GetByte(y, 0, len(y), i)
 decreases
 pure func ConstantTimeCompare(x, y []byte) (res int)
diff --git a/verification/dependencies/hash/hash.gobra b/verification/dependencies/hash/hash.gobra
index 339466fb6..e8c23f096 100644
--- a/verification/dependencies/hash/hash.gobra
+++ b/verification/dependencies/hash/hash.gobra
@@ -8,7 +8,9 @@
 
 package hash
 
-import "io"
+// As Gobra doesn't support embedding imported types yet, we have to define
+// `ScionHashSpec` here; consequently, there is no way around importing `io`.
+import "github.com/scionproto/scion/verification/io"
 
 // Hash is the common interface implemented by all hash functions.
 //
@@ -29,6 +31,9 @@ import "io"
 type Hash interface {
 	pred Mem()
 
+	// Due to Gobra issue #959, we need to repeat `pred AsidMem()` here.
+	pred AsidMem()
+
 	// Write (via the embedded io.Writer interface) adds more data to the running hash.
 	// It never returns an error.
 
@@ -71,3 +76,29 @@ type Hash interface {
 	decreases
 	BlockSize() (res int)
 }
+
+// In order to adequately relate the abstract computation of a MAC tag (using
+// `io.nextMsgtermSpec`) to the concrete computation (using `path.FullMAC` and 
+// `path.MAC`), we need to relate the key used by `io.nextMsgtermSpec` -- which 
+// is simply "indexed" by the AS identifier -- to the key used by the `Hash` 
+// instance passed to `path.FullMAC`/`path.MAC` (VerifiedSCION uses a keyed hash). 
+// To this end, during the creation of the `Hash` instance, we not only pass
+// the key but also the associated AS ID (cf. `scrypto.InitMac`) which can then
+// later be accessed using `Asid()`.
+// As this specification is specific to VerifiedSCION, we don't add it to `Hash`
+// directly, but instead in this interface which embeds `Hash`.
+type ScionHashSpec interface {
+	Hash
+
+	// Due to Gobra issue #958, we need to repeat `pred Mem()` here.
+	pred Mem()
+
+	// Memory footprint for `Asid`. Needed s.t. we can establish that the result
+	// of `Asid()` does not change after a call to `Write` or `Reset`.
+	pred AsidMem()
+
+	ghost
+	requires AsidMem()
+	decreases
+	pure Asid() (ghost io.AS)
+}