diff --git a/pkg/addr/fmt.go b/pkg/addr/fmt.go
index f534b82ea..a86f617fd 100644
--- a/pkg/addr/fmt.go
+++ b/pkg/addr/fmt.go
@@ -112,6 +112,7 @@ func FormatAS(as_ AS, opts ...FormatOption) string {
 }
 
 // @ requires as_.inRange()
+// @ requires low(as_)
 // @ decreases
 func fmtAS(as_ AS, sep string) string {
 	if !as_.inRange() {
@@ -132,6 +133,7 @@ func fmtAS(as_ AS, sep string) string {
 	// @ b.ZeroBuilderIsReadyToUse()
 	b.Grow(maxLen)
 	// @ invariant b.Mem()
+	// @ invariant low(i)
 	// @ decreases asParts - i
 	for i := 0; i < asParts; i++ {
 		if i > 0 {
diff --git a/pkg/addr/host.go b/pkg/addr/host.go
index ce971e76c..e4464cf83 100644
--- a/pkg/addr/host.go
+++ b/pkg/addr/host.go
@@ -47,6 +47,7 @@ const (
 	HostTypeSVC
 )
 
+// @ requires low(t)
 // @ requires isValidHostAddrType(t)
 // @ decreases
 func (t HostAddrType) String() string {
@@ -91,6 +92,14 @@ const (
 type HostAddr interface {
 	//@ pred Mem()
 
+	// Return whether all the underlying data that needs to be low for the
+	// computation of `Pack`, `IP`, `String` is low.
+	// TODO: Once Gobra issue #955 is resolved, mark as `hyper`.
+	//@ ghost
+	//@ requires Mem()
+	//@ decreases
+	//@ pure IsLow() bool
+
 	//@ preserves acc(Mem(), R13)
 	//@ decreases
 	Size() int
@@ -99,12 +108,12 @@ type HostAddr interface {
 	//@ decreases
 	Type() HostAddrType
 
-	//@ requires acc(Mem(), R13)
+	//@ requires acc(Mem(), R13) && IsLow()
 	//@ ensures forall i int :: { &res[i] } 0 <= i && i < len(res) ==> acc(&res[i], R13)
 	//@ decreases
 	Pack() (res []byte)
 
-	//@ requires acc(Mem(), R13)
+	//@ requires acc(Mem(), R13) && IsLow()
 	//@ ensures forall i int :: { &res[i] } 0 <= i && i < len(res) ==> acc(&res[i], R13)
 	//@ decreases
 	IP() (res net.IP)
@@ -114,6 +123,7 @@ type HostAddr interface {
 	//@ decreases
 	Copy() (res HostAddr)
 
+	//@ requires  low(typeOf(o))
 	//@ preserves acc(Mem(), R13) && acc(o.Mem(), R13)
 	//@ decreases
 	Equal(o HostAddr) bool
@@ -123,7 +133,8 @@ type HostAddr interface {
 	// replaced by the String() method which is the one that should be implemented
 	//fmt.Stringer
 
-	//@ preserves acc(Mem(), R13)
+	//@ requires acc(Mem(), R13) && IsLow()
+	//@ ensures  acc(Mem(), R13)
 	//@ decreases
 	String() string
 }
@@ -163,14 +174,16 @@ func (h HostNone) Copy() (res HostAddr) {
 	return tmp
 }
 
-// @ ensures res == (typeOf(o) == type[HostNone])
+// The Viper encoding branches on `typeOf(o)`.
+// @ requires low(typeOf(o))
+// @ ensures  res == (typeOf(o) == type[HostNone])
 // @ decreases
 func (h HostNone) Equal(o HostAddr) (res bool) {
 	_, ok := o.(HostNone)
 	return ok
 }
 
-// @decreases
+// @ decreases
 func (h HostNone) String() string {
 	return "<None>"
 }
@@ -189,21 +202,28 @@ func (h HostIPv4) Type() HostAddrType {
 	return HostTypeIPv4
 }
 
-// @ requires acc(h.Mem(), R13)
+// @ requires acc(h.Mem(), R13) && h.IsLow()
 // @ ensures forall i int :: { &res[i] } 0 <= i && i < len(res) ==> acc(&res[i], R13)
 // @ decreases
 func (h HostIPv4) Pack() (res []byte) {
 	return []byte(h.IP())
 }
 
-// @ requires acc(h.Mem(), R13)
+// @ requires acc(h.Mem(), R13) && h.IsLow()
 // @ ensures forall i int :: { &res[i] }{ &h[i] } 0 <= i && i < len(res) ==> acc(&res[i], R13) && &res[i] == &h[i]
 // @ ensures len(res) == HostLenIPv4
 // @ decreases
 func (h HostIPv4) IP() (res net.IP) {
 	// XXX(kormat): ensure the reply is the 4-byte representation.
-	//@ unfold acc(h.Mem(), R13)
-	//@ unfold acc(sl.Bytes(h, 0, len(h)), R13)
+	//@ h.RevealIsLow(R13)
+	//@ unfold acc(h.Mem(), R13/2)
+	//@ assert forall i int :: { h.GetByte(i) } 0 <= i && i < len(h) ==>
+	//@ 	sl.GetByte(h, 0, len(h), i) == h.GetByte(i)
+	//@ unfold acc(sl.Bytes(h, 0, len(h)), R13/2)
+	//@ assert forall i int :: { &h[i] } 0 <= i && i < len(h) ==> 
+	//@ 	h.GetByte(i) == h[i]
+	//@ unfold acc(h.Mem(), R13/2)
+	//@ unfold acc(sl.Bytes(h, 0, len(h)), R13/2)
 	return net.IP(h).To4( /*@ false @*/ )
 }
 
@@ -221,6 +241,7 @@ func (h HostIPv4) Copy() (res HostAddr) {
 	return tmp
 }
 
+// @ requires  low(typeOf(o))
 // @ preserves acc(h.Mem(), R13)
 // @ preserves acc(o.Mem(), R13)
 // @ decreases
@@ -233,7 +254,8 @@ func (h HostIPv4) Equal(o HostAddr) bool {
 	return ok && net.IP(h).Equal(net.IP(ha))
 }
 
-// @ preserves acc(h.Mem(), R13)
+// @ requires acc(h.Mem(), R13) && h.IsLow()
+// @ ensures  acc(h.Mem(), R13)
 // @ decreases
 func (h HostIPv4) String() string {
 	//@ assert unfolding acc(h.Mem(), R13) in len(h) == HostLenIPv4
@@ -289,6 +311,7 @@ func (h HostIPv6) Copy() (res HostAddr) {
 	return tmp
 }
 
+// @ requires  low(typeOf(o))
 // @ preserves acc(h.Mem(), R13)
 // @ preserves acc(o.Mem(), R13)
 // @ decreases
@@ -318,6 +341,7 @@ type HostSVC uint16
 // SVC addresses, use BS_A, PS_A, CS_A, and SB_A; shorthand versions without
 // the _A suffix (e.g., PS) also return anycast SVC addresses. For multicast,
 // use BS_M, PS_M, CS_M, and SB_M.
+// @ requires low(str)
 // @ decreases
 func HostSVCFromString(str string) HostSVC {
 	var m HostSVC
@@ -373,13 +397,15 @@ func (h HostSVC) IP() (res net.IP) {
 	return nil
 }
 
+// @ ensures low(h) ==> low(res)
 // @ decreases
-func (h HostSVC) IsMulticast() bool {
+func (h HostSVC) IsMulticast() (res bool) {
 	return (h & SVCMcast) != 0
 }
 
+// @ ensures low(h) ==> low(res)
 // @ decreases
-func (h HostSVC) Base() HostSVC {
+func (h HostSVC) Base() (res HostSVC) {
 	return h & ^SVCMcast
 }
 
@@ -395,14 +421,18 @@ func (h HostSVC) Copy() (res HostAddr) {
 	return h
 }
 
+// @ requires low(typeOf(o))
 // @ decreases
 func (h HostSVC) Equal(o HostAddr) bool {
 	ha, ok := o.(HostSVC)
 	return ok && h == ha
 }
 
+// @ requires acc(h.Mem(), R13) && h.IsLow()
+// @ ensures  acc(h.Mem(), R13)
 // @ decreases
 func (h HostSVC) String() string {
+	//@ h.RevealIsLow(R13)
 	name := h.BaseString()
 	cast := 'A'
 	if h.IsMulticast() {
@@ -413,6 +443,7 @@ func (h HostSVC) String() string {
 
 // BaseString returns the upper case name of the service. For hosts or unrecognized services, it
 // returns UNKNOWN.
+// @ requires low(h)
 // @ decreases
 func (h HostSVC) BaseString() string {
 	switch h.Base() {
@@ -432,6 +463,7 @@ func (h HostSVC) Network() string {
 	return ""
 }
 
+// @ requires low(htype)
 // @ requires acc(b)
 // @ requires isValidHostAddrType(htype)
 // @ requires len(b) == sizeOfHostAddrType(htype)
@@ -475,7 +507,9 @@ func HostFromRaw(b []byte, htype HostAddrType) (res HostAddr, err error) {
 
 // @ requires acc(ip)
 // @ requires len(ip) == HostLenIPv4 || len(ip) == HostLenIPv6
-// @ ensures res.Mem()
+// @ requires low(len(ip)) && forall i int :: { &ip[i] } 0 <= i && i < len(ip) &&
+// @ 	low(i) ==> low(ip[i])
+// @ ensures  res.Mem()
 // @ decreases
 func HostFromIP(ip net.IP) (res HostAddr) {
 	if ip4 := ip.To4( /*@ false @*/ ); ip4 != nil {
@@ -490,7 +524,8 @@ func HostFromIP(ip net.IP) (res HostAddr) {
 	return tmp
 }
 
-// @ ensures res.Mem()
+// @ requires low(s)
+// @ ensures  res.Mem()
 // @ decreases
 func HostFromIPStr(s string) (res HostAddr) {
 	ip := net.ParseIP(s)
@@ -502,6 +537,7 @@ func HostFromIPStr(s string) (res HostAddr) {
 	return HostFromIP(ip)
 }
 
+// @ requires low(htype)
 // @ requires isValidHostAddrType(htype)
 // @ decreases
 func HostLen(htype HostAddrType) (uint8, error) {
@@ -521,6 +557,7 @@ func HostLen(htype HostAddrType) (uint8, error) {
 	return length, nil
 }
 
+// @ requires low(t)
 // @ decreases
 func HostTypeCheck(t HostAddrType) bool {
 	switch t {
diff --git a/pkg/addr/host_spec.gobra b/pkg/addr/host_spec.gobra
index 4108094ab..975fe6ffe 100644
--- a/pkg/addr/host_spec.gobra
+++ b/pkg/addr/host_spec.gobra
@@ -25,6 +25,13 @@ import (
 
 pred (h HostNone) Mem() { len(h) == HostLenNone }
 
+ghost
+requires h.Mem()
+decreases
+pure func (h HostNone) IsLow() bool {
+	return true
+}
+
 HostNone implements HostAddr
 
 pred (h HostIPv4) Mem() {
@@ -32,6 +39,33 @@ pred (h HostIPv4) Mem() {
 	slices.Bytes(h, 0, len(h))
 }
 
+ghost
+requires h.Mem()
+requires 0 <= i && i < len(h)
+decreases
+pure func (h HostIPv4) GetByte(i int) byte {
+	return unfolding h.Mem() in slices.GetByte(h, 0, len(h), i)
+}
+
+// TODO: Once Gobra issue #846 is resolved, implement this.
+ghost
+trusted
+requires h.Mem()
+decreases
+pure func (h HostIPv4) IsLow() bool
+
+// "Reveal the body" of `h.IsLow` (necessary bc. we can't implement `h.IsLow` yet).
+// TODO: Once Gobra issue #846 is resolved, implement this.
+ghost
+trusted
+requires p > 0
+requires acc(h.Mem(), p) && h.IsLow()
+ensures  acc(h.Mem(), p)
+ensures  low(len(h)) && forall i int :: { h.GetByte(i) } 0 <= i && i < len(h) &&
+	low(i) ==> low(h.GetByte(i))
+decreases
+func (h HostIPv4) RevealIsLow(p perm)
+
 HostIPv4 implements HostAddr
 
 pred (h HostIPv6) Mem() {
@@ -39,10 +73,34 @@ pred (h HostIPv6) Mem() {
 	slices.Bytes(h, 0, len(h))
 }
 
+ghost
+requires h.Mem()
+decreases
+pure func (h HostIPv6) IsLow() bool { 
+	return true
+}
+
 HostIPv6 implements HostAddr
 
 pred (h HostSVC) Mem() { true }
 
+// TODO: Once Gobra issue #846 is resolved, actually implement `IsLow`.
+ghost
+trusted
+requires h.Mem()
+decreases
+pure func (h HostSVC) IsLow() bool
+
+// "Reveal the body" of `h.IsLow` (necessary bc. we can't implement `h.IsLow` yet).
+// TODO: Once Gobra issue #846 is resolved, implement this.
+ghost
+trusted
+requires p > 0
+requires acc(h.Mem(), p) && h.IsLow()
+ensures  acc(h.Mem(), p) && low(h)
+decreases
+func (h HostSVC) RevealIsLow(p perm)
+
 HostSVC implements HostAddr
 
 pred (h *HostSVC) Mem() { acc(h) }
diff --git a/pkg/addr/isdas.go b/pkg/addr/isdas.go
index 2cb08c6b8..8f536a334 100644
--- a/pkg/addr/isdas.go
+++ b/pkg/addr/isdas.go
@@ -25,6 +25,7 @@ import (
 	"strings"
 
 	"github.com/scionproto/scion/pkg/private/serrors"
+	//@ "github.com/scionproto/scion/verification/utils/sif"
 )
 
 const (
@@ -48,8 +49,10 @@ type ISD uint16
 
 // ParseISD parses an ISD from a decimal string. Note that ISD 0 is parsed
 // without any errors.
+// @ requires low(s)
+// @ ensures  low(retISD) && low(retErr != nil)
 // @ decreases
-func ParseISD(s string) (ISD, error) {
+func ParseISD(s string) (retISD ISD, retErr error) {
 	isd, err := strconv.ParseUint(s, 10, ISDBits)
 	if err != nil {
 		return 0, serrors.WrapStr("parsing ISD", err)
@@ -71,13 +74,17 @@ type AS uint64
 
 // ParseAS parses an AS from a decimal (in the case of the 32bit BGP AS number
 // space) or ipv6-style hex (in the case of SCION-only AS numbers) string.
-// @ ensures retErr == nil ==> retAs.inRange()
+// @ requires low(_as)
+// @ ensures  retErr == nil ==> retAs.inRange()
+// @ ensures  low(retAs) && low(retErr != nil)
 // @ decreases
 func ParseAS(_as string) (retAs AS, retErr error) {
 	return parseAS(_as, ":")
 }
 
-// @ ensures retErr == nil ==> retAs.inRange()
+// @ requires low(_as) && low(sep)
+// @ ensures  retErr == nil ==> retAs.inRange()
+// @ ensures  low(retAs) && low(retErr != nil)
 // @ decreases
 func parseAS(_as string, sep string) (retAs AS, retErr error) {
 	parts := strings.Split(_as, sep)
@@ -92,6 +99,9 @@ func parseAS(_as string, sep string) (retAs AS, retErr error) {
 	var parsed AS
 	//@ invariant 0 <= i && i <= asParts
 	//@ invariant acc(parts)
+	//@ invariant forall i int :: { parts[i] } 0 <= i && i < len(parts) && 
+	//@ 	low(i) ==> low(parts[i])
+	//@ invariant low(i) && low(_as) && low(parsed)
 	//@ decreases asParts - i
 	for i := 0; i < asParts; i++ {
 		parsed <<= asPartBits
@@ -110,7 +120,9 @@ func parseAS(_as string, sep string) (retAs AS, retErr error) {
 	return parsed, nil
 }
 
-// @ ensures retErr == nil ==> retAs.inRange()
+// @ requires low(s)
+// @ ensures  retErr == nil ==> retAs.inRange()
+// @ ensures  low(retAs) && low(retErr != nil)
 // @ decreases
 func asParseBGP(s string) (retAs AS, retErr error) {
 	_as, err := strconv.ParseUint(s, 10, BGPASBits)
@@ -132,6 +144,7 @@ func asParseBGP(s string) (retAs AS, retErr error) {
 }
 
 // @ requires _as.inRange()
+// @ requires low(_as)
 // @ decreases
 func (_as AS) String() string {
 	return fmtAS(_as, ":")
@@ -143,6 +156,7 @@ func (_as AS) inRange() bool {
 	return _as <= MaxAS
 }
 
+// @ requires low(_as)
 // @ decreases
 func (_as AS) MarshalText() ([]byte, error) {
 	if !_as.inRange() {
@@ -152,10 +166,14 @@ func (_as AS) MarshalText() ([]byte, error) {
 	return []byte(_as.String()), nil
 }
 
+// @ requires  forall i int :: { &text[i] } 0 <= i && i < len(text) ==> acc(&text[i])
+// @ requires  low(len(text)) && forall i int :: { text[i] } 0 <= i && i < len(text) &&
+// @ 	low(i) ==> low(text[i])
 // @ preserves acc(_as)
-// @ preserves forall i int :: { &text[i] } 0 <= i && i < len(text) ==> acc(&text[i])
+// @ ensures   forall i int :: { &text[i] } 0 <= i && i < len(text) ==> acc(&text[i])
 // @ decreases
 func (_as *AS) UnmarshalText(text []byte) error {
+	//@ sif.LowSliceImpliesLowString(text, writePerm)
 	parsed, err := ParseAS(string(text))
 	if err != nil {
 		return err
@@ -176,8 +194,9 @@ type IA uint64
 // is encountered. Callers must ensure that the values passed to this function
 // are valid.
 // @ requires _as.inRange()
+// @ ensures  low(isd) && low(_as) ==> low(res)
 // @ decreases
-func MustIAFrom(isd ISD, _as AS) IA {
+func MustIAFrom(isd ISD, _as AS) (res IA) {
 	ia, err := IAFrom(isd, _as)
 	if err != nil {
 		panic(fmt.Sprintf("parsing ISD-AS: %s", err))
@@ -187,7 +206,8 @@ func MustIAFrom(isd ISD, _as AS) IA {
 
 // IAFrom creates an IA from the ISD and AS number.
 // @ requires _as.inRange()
-// @ ensures err == nil
+// @ ensures  err == nil
+// @ ensures  low(isd) && low(_as) ==> low(ia)
 // @ decreases
 func IAFrom(isd ISD, _as AS) (ia IA, err error) {
 	if !_as.inRange() {
@@ -197,8 +217,10 @@ func IAFrom(isd ISD, _as AS) (ia IA, err error) {
 }
 
 // ParseIA parses an IA from a string of the format 'isd-as'.
+// @ requires low(ia)
+// @ ensures  low(retErr != nil)
 // @ decreases
-func ParseIA(ia string) (IA, error) {
+func ParseIA(ia string) (retIA IA, retErr error) {
 	parts := strings.Split(ia, "-")
 	if len(parts) != 2 {
 		return 0, serrors.New("invalid ISD-AS", "value", ia)
@@ -214,13 +236,15 @@ func ParseIA(ia string) (IA, error) {
 	return MustIAFrom(isd, _as), nil
 }
 
+// @ ensures low(ia) ==> low(res)
 // @ decreases
-func (ia IA) ISD() ISD {
+func (ia IA) ISD() (res ISD) {
 	return ISD(ia >> ASBits)
 }
 
+// @ ensures low(ia) ==> low(res)
 // @ decreases
-func (ia IA) AS() AS {
+func (ia IA) AS() (res AS) {
 	return AS(ia) & MaxAS
 }
 
@@ -229,10 +253,14 @@ func (ia IA) MarshalText() ([]byte, error) {
 	return []byte(ia.String()), nil
 }
 
+// @ requires  forall i int :: { &b[i] } 0 <= i && i < len(b) ==> acc(&b[i])
+// @ requires  low(len(b)) && forall i int :: { b[i] } 0 <= i && i < len(b) &&
+// @ 	low(i) ==> low(b[i])
 // @ preserves acc(ia)
-// @ preserves forall i int :: { &b[i] } 0 <= i && i < len(b) ==> acc(&b[i])
+// @ ensures   forall i int :: { &b[i] } 0 <= i && i < len(b) ==> acc(&b[i])
 // @ decreases
 func (ia *IA) UnmarshalText(b []byte) error {
+	//@ sif.LowSliceImpliesLowString(b, writePerm)
 	parsed, err := ParseIA(string(b))
 	if err != nil {
 		return err
@@ -253,6 +281,8 @@ func (ia IA) Equal(other IA) bool {
 }
 
 // IsWildcard returns whether the ia has a wildcard part (isd or as).
+// Due to short-circuit evaluation, this branches on `ia.ISD() == 0`.
+// @ requires low(ia)
 // @ decreases
 func (ia IA) IsWildcard() bool {
 	return ia.ISD() == 0 || ia.AS() == 0
@@ -265,6 +295,7 @@ func (ia IA) String() string {
 }
 
 // Set implements flag.Value interface
+// @ requires  low(s)
 // @ preserves acc(ia)
 // @ decreases
 func (ia *IA) Set(s string) 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/empty/empty.go b/pkg/slayers/path/empty/empty.go
index 30b7c12ed..36f2705dd 100644
--- a/pkg/slayers/path/empty/empty.go
+++ b/pkg/slayers/path/empty/empty.go
@@ -55,6 +55,7 @@ func RegisterPath() {
 // bytes on the wire and is used for AS internal communication.
 type Path struct{}
 
+// @ requires low(len(r))
 // @ ensures  len(r) == 0 ==> (e == nil && o.Mem(r))
 // @ ensures  len(r) != 0 ==> (e != nil && e.ErrorMem() && o.NonInitMem())
 // @ decreases
diff --git a/pkg/slayers/path/empty/empty_spec.gobra b/pkg/slayers/path/empty/empty_spec.gobra
index a4bd86d16..757e3455a 100644
--- a/pkg/slayers/path/empty/empty_spec.gobra
+++ b/pkg/slayers/path/empty/empty_spec.gobra
@@ -46,9 +46,17 @@ pure func (p Path) LenSpec(ghost ub []byte) (l int) {
 	return PathLen
 }
 
+ghost
+requires p.Mem(ub)
+decreases
+pure func (p Path) IsLow(ub []byte) bool {
+	return true
+}
+
 Path implements path.Path
 
 // Definitions to allow *Path to be treated as a path.Path
 pred (e *Path) Mem(buf []byte) { acc(e) && len(buf) == 0 }
 pred (e *Path) NonInitMem() { true }
+
 (*Path) implements path.Path
\ No newline at end of file
diff --git a/pkg/slayers/path/epic/epic.go b/pkg/slayers/path/epic/epic.go
index 4884f5162..d71979af5 100644
--- a/pkg/slayers/path/epic/epic.go
+++ b/pkg/slayers/path/epic/epic.go
@@ -78,9 +78,12 @@ type Path struct {
 
 // SerializeTo serializes the Path into buffer b. On failure, an error is returned, otherwise
 // SerializeTo will return nil.
-// @ preserves acc(p.Mem(ubuf), R1)
+// @ requires  low(len(b))
+// @ requires  acc(p.Mem(ubuf), R1)
+// @ requires  p.IsLow(ubuf)
 // @ preserves sl.Bytes(ubuf, 0, len(ubuf))
 // @ preserves sl.Bytes(b, 0, len(b))
+// @ ensures   acc(p.Mem(ubuf), R1)
 // @ ensures   r != nil ==> r.ErrorMem()
 // @ ensures   !old(p.hasScionPath(ubuf)) ==> r != nil
 // @ ensures   len(b) < old(p.LenSpec(ubuf)) ==> r != nil
@@ -88,6 +91,7 @@ type Path struct {
 // @ ensures   old(p.getLHVFLen(ubuf)) != HVFLen ==> r != nil
 // @ decreases
 func (p *Path) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) {
+	//@ p.RevealIsLow(ubuf)
 	if len(b) < p.Len( /*@ ubuf @*/ ) {
 		return serrors.New("buffer too small to serialize path.", "expected", int(p.Len( /*@ ubuf @*/ )),
 			"actual", len(b))
@@ -136,6 +140,7 @@ func (p *Path) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) {
 // DecodeFromBytes deserializes the buffer b into the Path. On failure, an error is returned,
 // otherwise SerializeTo will return nil.
 // @ requires  p.NonInitMem()
+// @ requires  low(len(b))
 // @ preserves acc(sl.Bytes(b, 0, len(b)), R42)
 // @ ensures   len(b) < MetadataLen ==> r != nil
 // @ ensures   r == nil ==> p.Mem(b)
@@ -211,6 +216,7 @@ func (p *Path) Reverse( /*@ ghost ubuf []byte @*/ ) (ret path.Path, r error) {
 // Len returns the length of the EPIC path in bytes.
 // @ preserves acc(p.Mem(ubuf), R50)
 // @ ensures   l == p.LenSpec(ubuf)
+// @ ensures   low(l)
 // @ decreases
 func (p *Path) Len( /*@ ghost ubuf []byte @*/ ) (l int) {
 	// @ unfold acc(p.Mem(ubuf), R50)
diff --git a/pkg/slayers/path/epic/epic_spec.gobra b/pkg/slayers/path/epic/epic_spec.gobra
index 950ceb4b1..cf4b768fe 100644
--- a/pkg/slayers/path/epic/epic_spec.gobra
+++ b/pkg/slayers/path/epic/epic_spec.gobra
@@ -102,4 +102,20 @@ pure func (p *Path) IsValidResultOfDecoding(b []byte) (res bool) {
 	return true
 }
 
-(*Path) implements path.Path
\ No newline at end of file
+(*Path) implements path.Path
+
+// TODO: Once Gobra issue #846 is resolved, actually implement `IsLow`.
+ghost
+trusted
+requires p.Mem(ub)
+decreases
+pure func (p *Path) IsLow(ub []byte) bool
+
+// TODO: Once Gobra issue #846 is resolved, actually implement this.
+ghost
+trusted
+requires acc(p.Mem(ub), R2) && p.IsLow(ub)
+ensures  acc(p.Mem(ub), R2)
+ensures  low(p.getPHVFLen(ub)) && low(p.getLHVFLen(ub))
+decreases
+func (p *Path) RevealIsLow(ub []byte)
diff --git a/pkg/slayers/path/hopfield.go b/pkg/slayers/path/hopfield.go
index 03299dbb4..e9e75e06b 100644
--- a/pkg/slayers/path/hopfield.go
+++ b/pkg/slayers/path/hopfield.go
@@ -79,7 +79,7 @@ type HopField struct {
 // @ preserves acc(sl.Bytes(raw, 0, HopLen), R45)
 // @ ensures   h.Mem()
 // @ ensures   err == nil
-// @ ensures  BytesToIO_HF(raw, 0, 0, HopLen) ==
+// @ ensures   BytesToIO_HF(raw, 0, 0, HopLen) ==
 // @ 	unfolding acc(h.Mem(), R10) in h.Abs()
 // @ decreases
 func (h *HopField) DecodeFromBytes(raw []byte) (err error) {
@@ -110,13 +110,15 @@ func (h *HopField) DecodeFromBytes(raw []byte) (err error) {
 // SerializeTo writes the fields into the provided buffer. The buffer must be of length >=
 // path.HopLen.
 // @ requires  len(b) >= HopLen
-// @ preserves acc(h.Mem(), R10)
+// @ requires  acc(h.Mem(), R10) && h.IsLow()
 // @ preserves sl.Bytes(b, 0, HopLen)
+// @ ensures   acc(h.Mem(), R10)
 // @ ensures   err == nil
-// @ ensures  BytesToIO_HF(b, 0, 0, HopLen) ==
+// @ ensures   BytesToIO_HF(b, 0, 0, HopLen) ==
 // @ 	unfolding acc(h.Mem(), R10) in h.Abs()
 // @ decreases
 func (h *HopField) SerializeTo(b []byte) (err error) {
+	//@ h.RevealIsLow(R10)
 	if len(b) < HopLen {
 		return serrors.New("buffer for HopField too short", "expected", MacLen, "actual", len(b))
 	}
diff --git a/pkg/slayers/path/hopfield_spec.gobra b/pkg/slayers/path/hopfield_spec.gobra
index 816768b22..959c232aa 100644
--- a/pkg/slayers/path/hopfield_spec.gobra
+++ b/pkg/slayers/path/hopfield_spec.gobra
@@ -27,6 +27,37 @@ pred (h *HopField) Mem() {
 	acc(h) && h.ConsIngress >= 0 && h.ConsEgress >= 0
 }
 
+ghost
+requires h.Mem()
+decreases
+pure func (h *HopField) GetEgressRouterAlert() bool {
+	return unfolding h.Mem() in h.EgressRouterAlert
+}
+
+ghost
+requires h.Mem()
+decreases
+pure func (h *HopField) GetIngressRouterAlert() bool {
+	return unfolding h.Mem() in h.IngressRouterAlert
+}
+
+// TODO: Once Gobra issue #846 is resolved, implement this.
+ghost
+trusted
+requires h.Mem()
+decreases
+pure func (h *HopField) IsLow() bool
+
+// "Reveal the body" of `h.IsLow` (necessary bc. we can't implement `h.IsLow` yet).
+// TODO: Once Gobra issue #846 is resolved, implement this.
+ghost
+trusted
+requires p > 0
+requires acc(h.Mem(), p) && h.IsLow()
+ensures  acc(h.Mem(), p)
+ensures  low(h.GetEgressRouterAlert()) && low(h.GetIngressRouterAlert())
+decreases
+func (h *HopField) RevealIsLow(p perm)
 
 ghost
 decreases
diff --git a/pkg/slayers/path/infofield.go b/pkg/slayers/path/infofield.go
index 6f9e616aa..033369ff5 100644
--- a/pkg/slayers/path/infofield.go
+++ b/pkg/slayers/path/infofield.go
@@ -88,8 +88,10 @@ func (inf *InfoField) DecodeFromBytes(raw []byte) (err error) {
 // SerializeTo writes the fields into the provided buffer. The buffer must be of length >=
 // path.InfoLen.
 // @ requires  len(b) >= InfoLen
-// @ preserves acc(inf, R10)
+// @ requires  acc(inf, R10)
+// @ requires  low(inf.ConsDir) && low(inf.Peer)
 // @ preserves slices.Bytes(b, 0, len(b))
+// @ ensures   acc(inf, R10)
 // @ ensures   err == nil
 // @ ensures   inf.ToAbsInfoField() ==
 // @ 	BytesToAbsInfoField(b, 0)
diff --git a/pkg/slayers/path/mac.go b/pkg/slayers/path/mac.go
index df11254b7..f24e771c3 100644
--- a/pkg/slayers/path/mac.go
+++ b/pkg/slayers/path/mac.go
@@ -30,6 +30,7 @@ const MACBufferSize = 16
 // 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  low(len(buffer))
 // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer))
 // @ ensures   h.Mem()
 // @ decreases
@@ -47,6 +48,7 @@ func MAC(h hash.Hash, info InfoField, hf HopField, buffer []byte) [MacLen]byte {
 // 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  low(len(buffer))
 // @ preserves len(buffer) >= MACBufferSize ==> sl.Bytes(buffer, 0, len(buffer))
 // @ ensures   h.Mem()
 // @ ensures   len(res) == MACBufferSize && sl.Bytes(res, 0, MACBufferSize)
diff --git a/pkg/slayers/path/onehop/onehop.go b/pkg/slayers/path/onehop/onehop.go
index 31e832b34..bf0e1e44d 100644
--- a/pkg/slayers/path/onehop/onehop.go
+++ b/pkg/slayers/path/onehop/onehop.go
@@ -64,6 +64,7 @@ type Path struct {
 }
 
 // @ requires  o.NonInitMem()
+// @ requires  low(len(data))
 // @ preserves acc(sl.Bytes(data, 0, len(data)), R42)
 // @ ensures   (len(data) >= PathLen) == (r == nil)
 // @ ensures   r == nil ==> o.Mem(data)
@@ -98,20 +99,25 @@ func (o *Path) DecodeFromBytes(data []byte) (r error) {
 	return r
 }
 
-// @ preserves acc(o.Mem(ubuf), R1)
+// @ requires  low(len(b))
+// @ requires  acc(o.Mem(ubuf), R1) && o.IsLow(ubuf)
 // @ preserves acc(sl.Bytes(ubuf, 0, len(ubuf)), R1)
 // @ preserves sl.Bytes(b, 0, len(b))
+// @ ensures   acc(o.Mem(ubuf), R1)
 // @ ensures   (len(b) >= PathLen) == (err == nil)
 // @ ensures   err != nil ==> err.ErrorMem()
 // @ ensures   err == nil ==> o.LenSpec(ubuf) <= len(b)
 // @ decreases
 func (o *Path) SerializeTo(b []byte /*@, ubuf []byte @*/) (err error) {
+	//@ o.RevealIsLow(ubuf, R1)
 	if len(b) < PathLen {
 		return serrors.New("buffer too short for OneHop path", "expected", int(PathLen), "actual",
 			int(len(b)))
 	}
 	offset := 0
 	//@ unfold acc(o.Mem(ubuf), R1)
+	//@ o.FirstHop.RevealIsLow(R2)
+	//@ o.SecondHop.RevealIsLow(R2)
 	//@ sl.SplitRange_Bytes(b, 0, offset+path.InfoLen, writePerm)
 	if err := o.Info.SerializeTo(b[:offset+path.InfoLen]); err != nil {
 		//@ sl.CombineRange_Bytes(b, 0, offset+path.InfoLen, writePerm)
@@ -135,10 +141,13 @@ func (o *Path) SerializeTo(b []byte /*@, ubuf []byte @*/) (err error) {
 
 // ToSCIONDecoded converts the one hop path in to a normal SCION path in the
 // decoded format.
-// @ preserves o.Mem(ubuf)
+// @ requires  o.Mem(ubuf)
+// @ requires  low(o.GetSecondHopConsIngress(ubuf))
 // @ preserves sl.Bytes(ubuf, 0, len(ubuf))
+// @ ensures   o.Mem(ubuf)
 // @ ensures   err == nil ==> (sd != nil && sd.Mem(ubuf))
 // @ ensures   err != nil ==> err.ErrorMem()
+// @ ensures   low(err != nil)
 // @ decreases
 func (o *Path) ToSCIONDecoded( /*@ ghost ubuf []byte @*/ ) (sd *scion.Decoded, err error) {
 	//@ unfold acc(o.Mem(ubuf), R1)
@@ -198,14 +207,15 @@ func (o *Path) ToSCIONDecoded( /*@ ghost ubuf []byte @*/ ) (sd *scion.Decoded, e
 }
 
 // Reverse a OneHop path that returns a reversed SCION path.
-// @ requires o.Mem(ubuf)
+// @ requires  o.Mem(ubuf) && o.IsLow(ubuf)
 // @ preserves sl.Bytes(ubuf, 0, len(ubuf))
-// @ ensures err == nil ==> p != nil
-// @ ensures err == nil ==> p.Mem(ubuf)
-// @ ensures err == nil ==> typeOf(p) == type[*scion.Decoded]
-// @ ensures err != nil ==> err.ErrorMem()
+// @ ensures   err == nil ==> p != nil
+// @ ensures   err == nil ==> p.Mem(ubuf)
+// @ ensures   err == nil ==> typeOf(p) == type[*scion.Decoded]
+// @ ensures   err != nil ==> err.ErrorMem()
 // @ decreases
 func (o *Path) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, err error) {
+	//@ o.RevealIsLow(ubuf, writePerm)
 	sp, err := o.ToSCIONDecoded( /*@ ubuf @*/ )
 	if err != nil {
 		return nil, serrors.WrapStr("converting to scion path", err)
diff --git a/pkg/slayers/path/onehop/onehop_spec.gobra b/pkg/slayers/path/onehop/onehop_spec.gobra
index f81b9b982..c96e07370 100644
--- a/pkg/slayers/path/onehop/onehop_spec.gobra
+++ b/pkg/slayers/path/onehop/onehop_spec.gobra
@@ -32,6 +32,55 @@ pred (o *Path) Mem(ubuf []byte) {
 	PathLen <= len(ubuf)
 }
 
+ghost
+requires o.Mem(ub)
+decreases
+pure func (o *Path) GetSecondHopConsIngress(ghost ub []byte) uint16 {
+	return unfolding o.Mem(ub) in 
+		unfolding o.SecondHop.Mem() in o.SecondHop.ConsIngress
+}
+
+ghost
+requires o.Mem(ub)
+decreases
+pure func (o *Path) GetInfo(ghost ub []byte) path.InfoField {
+	return unfolding o.Mem(ub) in o.Info
+}
+
+ghost
+requires o.Mem(ub)
+decreases
+pure func (o *Path) FirstHopIsLow(ghost ub []byte) bool {
+	return unfolding o.Mem(ub) in o.FirstHop.IsLow()
+}
+
+ghost
+requires o.Mem(ub)
+decreases
+pure func (o *Path) SecondHopIsLow(ghost ub []byte) bool {
+	return unfolding o.Mem(ub) in o.SecondHop.IsLow()
+}
+
+// TODO: Once Gobra issue #846 is resolved, implement `IsLow`.
+ghost
+trusted
+requires o.Mem(ub)
+decreases
+pure func (o *Path) IsLow(ub []byte) bool
+
+// "Reveal the body" of `o.IsLow` (necessary bc. we can't implement `o.IsLow` yet).
+// TODO: Once Gobra issue #846 is resolved, implement this.
+ghost
+trusted
+requires p > 0
+requires acc(o.Mem(ub), p) && o.IsLow(ub)
+ensures  acc(o.Mem(ub), p)
+ensures  low(o.GetSecondHopConsIngress(ub)) &&
+	low(o.GetInfo(ub).ConsDir) && low(o.GetInfo(ub).Peer) &&
+	o.FirstHopIsLow(ub) && o.SecondHopIsLow(ub)
+decreases
+func (o *Path) RevealIsLow(ub []byte, p perm)
+
 ghost
 requires p.Mem(buf)
 ensures  p.NonInitMem()
@@ -64,4 +113,4 @@ pure func (p *Path) LenSpec(ghost ub []byte) int {
 	return PathLen
 }
 
-(*Path) implements path.Path
\ No newline at end of file
+(*Path) implements path.Path
diff --git a/pkg/slayers/path/path.go b/pkg/slayers/path/path.go
index 2d0bdc5af..1c5db34c5 100644
--- a/pkg/slayers/path/path.go
+++ b/pkg/slayers/path/path.go
@@ -53,7 +53,9 @@ func init() {
 type Type uint8
 
 // @ requires 0 <= t && t < maxPathType
-// @ preserves acc(PkgMem(), R20)
+// @ requires acc(PkgMem(), R20)
+// @ requires low(Registered(t))
+// @ ensures  acc(PkgMem(), R20)
 // @ decreases
 func (t Type) String() string {
 	//@ unfold acc(PkgMem(), R20)
@@ -72,12 +74,22 @@ type Path interface {
 	// (VerifiedSCION) Must imply the resources required to initialize
 	// a new instance of a predicate.
 	//@ pred NonInitMem()
+
+	// TODO: Once Gobra issue #955 is resolved, mark as `hyper`.
+	//@ ghost
+	//@ requires Mem(ub)
+	//@ decreases
+	//@ pure IsLow(ghost ub []byte) bool
+
 	// SerializeTo serializes the path into the provided buffer.
 	// (VerifiedSCION) There are implementations of this interface that modify the underlying
 	// structure when serializing (e.g. scion.Raw)
+	//@ requires  low(len(b))
+	//@ requires  acc(Mem(ub), R1)
+	//@ requires  IsLow(ub)
 	//@ preserves sl.Bytes(ub, 0, len(ub))
-	//@ preserves acc(Mem(ub), R1)
 	//@ preserves sl.Bytes(b, 0, len(b))
+	//@ ensures   acc(Mem(ub), R1)
 	//@ ensures   e != nil ==> e.ErrorMem()
 	//@ decreases
 	SerializeTo(b []byte /*@, ghost ub []byte @*/) (e error)
@@ -85,6 +97,7 @@ type Path interface {
 	// (VerifiedSCION) There are implementations of this interface (e.g., scion.Raw) that
 	// store b and use it as internal data.
 	//@ requires  NonInitMem()
+	//@ requires  low(len(b))
 	//@ preserves acc(sl.Bytes(b, 0, len(b)), R42)
 	//@ ensures   err == nil ==> Mem(b)
 	//@ ensures   err == nil ==> IsValidResultOfDecoding(b)
@@ -100,7 +113,7 @@ type Path interface {
 	//@ IsValidResultOfDecoding(b []byte) bool
 	// Reverse reverses a path such that it can be used in the reversed direction.
 	// XXX(shitz): This method should possibly be moved to a higher-level path manipulation package.
-	//@ requires  Mem(ub)
+	//@ requires  Mem(ub) && IsLow(ub)
 	//@ preserves sl.Bytes(ub, 0, len(ub))
 	//@ ensures   e == nil ==> p != nil
 	//@ ensures   e == nil ==> p.Mem(ub)
@@ -188,6 +201,7 @@ func StrictDecoding(strict bool) {
 // NewPath returns a new path object of pathType.
 // @ requires 0 <= pathType && pathType < maxPathType
 // @ requires acc(PkgMem(), _)
+// @ requires low(Registered(pathType)) && low(IsStrictDecoding())
 // @ ensures  e != nil ==> e.ErrorMem()
 // @ ensures  e == nil ==> p != nil && p.NonInitMem()
 // @ decreases
diff --git a/pkg/slayers/path/path_spec.gobra b/pkg/slayers/path/path_spec.gobra
index b22031a19..f96144402 100644
--- a/pkg/slayers/path/path_spec.gobra
+++ b/pkg/slayers/path/path_spec.gobra
@@ -31,6 +31,13 @@ pred (r *rawPath) NonInitMem() {
 	acc(r)
 }
 
+ghost
+requires r.Mem(ub)
+decreases
+pure func (r *rawPath) IsLow(ub []byte) bool {
+	return true
+}
+
 ghost
 requires p.Mem(buf)
 ensures  p.NonInitMem()
diff --git a/pkg/slayers/path/scion/decoded_spec.gobra b/pkg/slayers/path/scion/decoded_spec.gobra
index 1ebbce5a3..131d1a5d5 100644
--- a/pkg/slayers/path/scion/decoded_spec.gobra
+++ b/pkg/slayers/path/scion/decoded_spec.gobra
@@ -47,6 +47,13 @@ pred (d *Decoded) Mem(ubuf []byte) {
 	(forall i int :: { &d.HopFields[i] } 0 <= i && i < len(d.HopFields) ==> d.HopFields[i].Mem())
 }
 
+ghost
+requires d.Mem(ub)
+decreases
+pure func (d *Decoded) IsLow(ub []byte) bool {
+	return true
+}
+
 /**** End of Predicates ****/
 
 /**** Stubs ****/
@@ -112,6 +119,7 @@ ensures  e == nil ==> (
 	d.LenSpec(ubuf) == old(d.LenSpec(ubuf)) &&
 	(old(d.GetBase(ubuf).Valid()) ==> d.GetBase(ubuf).Valid()))
 ensures  e != nil ==> d.NonInitMem() && e.ErrorMem()
+ensures  low(e != nil)
 decreases
 func (d *Decoded) IncPath(ghost ubuf []byte) (e error) {
 	unfold d.Mem(ubuf)
diff --git a/pkg/slayers/path/scion/raw.go b/pkg/slayers/path/scion/raw.go
index 9947c338e..b8d869f26 100644
--- a/pkg/slayers/path/scion/raw.go
+++ b/pkg/slayers/path/scion/raw.go
@@ -41,6 +41,7 @@ type Raw struct {
 // @ 	s.GetBase(data).WeaklyValid() &&
 // @ 	s.GetBase(data).EqAbsHeader(data)
 // @ ensures   res != nil ==> (s.NonInitMem() && res.ErrorMem())
+// @ ensures   low(res == nil)
 // @ decreases
 func (s *Raw) DecodeFromBytes(data []byte) (res error) {
 	//@ unfold s.NonInitMem()
@@ -105,6 +106,7 @@ func (s *Raw) SerializeTo(b []byte /*@, ghost ubuf []byte @*/) (r error) {
 // @ ensures   err == nil ==> p != nil && p != (*Raw)(nil)
 // @ ensures   err == nil ==> p.Mem(ubuf)
 // @ ensures   err != nil ==> err.ErrorMem()
+// @ ensures   low(err != nil)
 // @ decreases
 func (s *Raw) Reverse( /*@ ghost ubuf []byte @*/ ) (p path.Path, err error) {
 	// XXX(shitz): The current implementation is not the most performant, since it parses the entire
diff --git a/pkg/slayers/path/scion/raw_spec.gobra b/pkg/slayers/path/scion/raw_spec.gobra
index 218a6a38e..613b3bf2f 100644
--- a/pkg/slayers/path/scion/raw_spec.gobra
+++ b/pkg/slayers/path/scion/raw_spec.gobra
@@ -37,6 +37,14 @@ pred (s *Raw) Mem(buf []byte) {
 	s.Raw === buf[:len(s.Raw)] &&
 	len(s.Raw) == s.Base.Len()
 }
+
+ghost
+requires s.Mem(ub)
+decreases
+pure func (s *Raw) IsLow(ub []byte) bool {
+	return true
+}
+
 /**** End of Predicates ****/
 
 (*Raw) implements path.Path
@@ -73,6 +81,7 @@ pure func (s *Raw) Type(ghost buf []byte) path.Type {
   */
 preserves acc(s.Mem(buf), R50)
 ensures   l == s.LenSpec(buf)
+ensures   low(l)
 decreases
 func (s *Raw) Len(ghost buf []byte) (l int) {
 	return unfolding acc(s.Mem(buf), _) in s.Base.Len()
diff --git a/private/topology/linktype.go b/private/topology/linktype.go
index d8b47579f..e7cdff685 100644
--- a/private/topology/linktype.go
+++ b/private/topology/linktype.go
@@ -23,6 +23,7 @@ import (
 	"github.com/scionproto/scion/pkg/private/serrors"
 	//@ . "github.com/scionproto/scion/verification/utils/definitions"
 	//@ sl "github.com/scionproto/scion/verification/utils/slices"
+	//@ "github.com/scionproto/scion/verification/utils/sif"
 )
 
 // LinkType describes inter-AS links.
@@ -44,6 +45,7 @@ const (
 	Peer LinkType = 4
 )
 
+// @ requires low(l)
 // @ decreases
 func (l LinkType) String() string {
 	if l == Unset {
@@ -59,6 +61,7 @@ func (l LinkType) String() string {
 
 // LinkTypeFromString returns the numerical link type associated with a string description. If the
 // string is not recognized, an Unset link type is returned. The matching is case-insensitive.
+// @ requires low(s)
 // @ decreases
 func LinkTypeFromString(s string) (res LinkType) {
 	var l /*@@@*/ LinkType
@@ -70,6 +73,7 @@ func LinkTypeFromString(s string) (res LinkType) {
 	return l
 }
 
+// @ requires low(l)
 // @ ensures (l == Core || l == Parent || l == Child || l == Peer) == (err == nil)
 // @ ensures err == nil ==> sl.Bytes(res, 0, len(res))
 // @ ensures err != nil ==> err.ErrorMem()
@@ -97,13 +101,21 @@ func (l LinkType) MarshalText() (res []byte, err error) {
 	}
 }
 
+// @ requires  acc(sl.Bytes(data, 0, len(data)), R15)
+// @ requires  low(len(data)) && 
+// @ 	forall i int :: { sl.GetByte(data, 0, len(data), i) } 0 <= i && i < len(data) && low(i) ==>
+// @ 		low(sl.GetByte(data, 0, len(data), i))
 // @ preserves acc(l)
-// @ preserves acc(sl.Bytes(data, 0, len(data)), R15)
+// @ ensures   acc(sl.Bytes(data, 0, len(data)), R15)
 // @ ensures   err != nil ==> err.ErrorMem()
+// @ ensures   low(err != nil)
 // @ decreases
 func (l *LinkType) UnmarshalText(data []byte) (err error) {
-	//@ unfold acc(sl.Bytes(data, 0, len(data)), R15)
-	//@ ghost defer fold acc(sl.Bytes(data, 0, len(data)), R15)
+	//@ unfold acc(sl.Bytes(data, 0, len(data)), R16)
+	//@ ghost defer fold acc(sl.Bytes(data, 0, len(data)), R16)
+	//@ assert forall i int :: { &data[i] } 0 <= i && i < len(data) ==>
+	//@ 	sl.GetByte(data, 0, len(data), i) == data[i]
+	//@ sif.LowSliceImpliesLowString(data, R16)
 	switch strings.ToLower(string(data)) {
 	case "core":
 		*l = Core
diff --git a/private/topology/underlay/defs.go b/private/topology/underlay/defs.go
index 9db9ca7e3..2885db386 100644
--- a/private/topology/underlay/defs.go
+++ b/private/topology/underlay/defs.go
@@ -47,7 +47,10 @@ const (
 	EndhostPort = 30041
 )
 
-func (o Type) String() string {
+// @ requires low(o)
+// @ requires o == UDPIPv4 || o == UDPIPv6 || o == UDPIPv46
+// @ ensures  low(res)
+func (o Type) String() (res string) {
 	switch o {
 	case UDPIPv4:
 		return UDPIPv4Name
@@ -56,11 +59,14 @@ func (o Type) String() string {
 	case UDPIPv46:
 		return UDPIPv46Name
 	default:
+		// @ Unreachable()
 		return fmt.Sprintf("UNKNOWN (%d)", o)
 	}
 }
 
-func TypeFromString(s string) (Type, error) {
+// @ requires low(s)
+// @ ensures  low(t) && low(err != nil)
+func TypeFromString(s string) (t Type, err error) {
 	switch strings.ToLower(s) {
 	case strings.ToLower(UDPIPv4Name):
 		return UDPIPv4, nil
@@ -94,7 +100,9 @@ func (ot Type) MarshalJSON() ([]byte, error) {
 	return json.Marshal(ot.String())
 }
 
-func (ot Type) IsUDP() bool {
+// @ requires low(ot)
+// @ ensures  low(res)
+func (ot Type) IsUDP() (res bool) {
 	switch ot {
 	case UDPIPv4, UDPIPv6, UDPIPv46:
 		return true
diff --git a/private/underlay/conn/conn.go b/private/underlay/conn/conn.go
index ad9611602..2a02e9a8c 100644
--- a/private/underlay/conn/conn.go
+++ b/private/underlay/conn/conn.go
@@ -43,6 +43,15 @@ type Messages []ipv4.Message
 // Conn describes the API for an underlay socket
 type Conn interface {
 	//@ pred Mem()
+
+	// Return whether all the underlying data that needs to be low for the
+	// computation of `WriteTo`, `Close` is low.
+	// TODO: Once Gobra issue #955 is resolved, mark as `hyper`.
+	//@ ghost
+	//@ requires Mem()
+	//@ decreases
+	//@ pure IsLow() bool
+
 	// (VerifiedSCION) Reads a message to b. Returns the number of read bytes.
 	//@ requires  acc(Mem(), _)
 	//@ preserves sl.Bytes(b, 0, len(b))
@@ -61,7 +70,7 @@ type Conn interface {
 	//@ ensures   err != nil ==> err.ErrorMem()
 	Write(b []byte) (n int, err error)
 	//@ requires  acc(u.Mem(), _)
-	//@ requires  acc(Mem(), _)
+	//@ requires  acc(Mem(), _) && IsLow()
 	//@ preserves acc(sl.Bytes(b, 0, len(b)), R10)
 	//@ ensures   err == nil ==> 0 <= n && n <= len(b)
 	//@ ensures   err != nil ==> err.ErrorMem()
@@ -91,7 +100,7 @@ type Conn interface {
 	//@ ensures   err != nil ==> err.ErrorMem()
 	//@ decreases
 	SetDeadline(time.Time) (err error)
-	//@ requires Mem()
+	//@ requires Mem() && IsLow()
 	//@ ensures  err != nil ==> err.ErrorMem()
 	//@ decreases
 	Close() (err error)
@@ -112,8 +121,9 @@ type Config struct {
 // The config can be used to customize socket behavior.
 // @ requires cfg.Mem()
 // @ requires listen != nil || remote != nil
-// @ requires listen != nil ==> acc(listen.Mem(), R10)
-// @ requires remote != nil ==> acc(remote.Mem(), R10)
+// @ requires listen != nil ==> acc(listen.Mem(), R10) && listen.IsLow()
+// @ requires remote != nil ==> acc(remote.Mem(), R10) && remote.IsLow()
+// @ requires low(listen != nil) && low(remote != nil) && cfg.IsLow()
 // @ ensures  e == nil ==> res.Mem()
 // @ ensures  e != nil ==> e.ErrorMem()
 // @ decreases
@@ -127,9 +137,11 @@ func New(listen, remote *net.UDPAddr, cfg *Config) (res Conn, e error) {
 	}
 	// @ assert remote != nil ==> a == remote
 	// @ assert remote == nil ==> a == listen
+	// @ a.RevealIsLow()
 	// @ unfold acc(a.Mem(), R15)
 	// @ unfold acc(sl.Bytes(a.IP, 0, len(a.IP)), R15)
-	// @ assert forall i int :: { &a.IP[i] } 0 <= i && i < len(a.IP) ==> acc(&a.IP[i], R15)
+	// @ assert forall i int :: { &a.IP[i] } 0 <= i && i < len(a.IP) ==>
+	// @ 	a.GetIPByte(i) == a.IP[i]
 	if a.IP.To4( /*@ false @*/ ) != nil {
 		return newConnUDPIPv4(listen, remote, cfg)
 	}
@@ -142,8 +154,9 @@ type connUDPIPv4 struct {
 }
 
 // @ requires cfg.Mem()
-// @ requires listen != nil ==> acc(listen.Mem(), _)
-// @ requires remote != nil ==> acc(remote.Mem(), _)
+// @ requires listen != nil ==> acc(listen.Mem(), _) && listen.IsLow()
+// @ requires remote != nil ==> acc(remote.Mem(), _) && remote.IsLow()
+// @ requires low(listen != nil) && low(remote != nil) && cfg.IsLow()
 // @ ensures  e == nil ==> res.Mem()
 // @ ensures  e != nil ==> e.ErrorMem()
 // @ decreases
@@ -216,8 +229,9 @@ type connUDPIPv6 struct {
 }
 
 // @ requires cfg.Mem()
-// @ requires listen != nil ==> acc(listen.Mem(), _)
-// @ requires remote != nil ==> acc(remote.Mem(), _)
+// @ requires listen != nil ==> acc(listen.Mem(), _) && listen.IsLow()
+// @ requires remote != nil ==> acc(remote.Mem(), _) && remote.IsLow()
+// @ requires low(listen != nil) && low(remote != nil) && cfg.IsLow()
 // @ ensures  e == nil ==> res.Mem()
 // @ ensures  e != nil ==> e.ErrorMem()
 // @ decreases
@@ -292,11 +306,13 @@ type connUDPBase struct {
 }
 
 // @ requires acc(cc)
-// @ requires laddr != nil ==> acc(laddr.Mem(), _)
-// @ requires raddr != nil ==> acc(raddr.Mem(), _)
+// @ requires laddr != nil ==> acc(laddr.Mem(), _) && laddr.IsLow()
+// @ requires raddr != nil ==> acc(raddr.Mem(), _) && raddr.IsLow()
 // @ requires cfg.Mem()
+// @ requires low(network) && low(laddr != nil) && low(raddr != nil) && cfg.IsLow()
 // @ ensures  errRet == nil ==> cc.Mem()
 // @ ensures  errRet != nil ==> errRet.ErrorMem()
+// @ ensures  low(errRet != nil)
 // @ decreases
 func (cc *connUDPBase) initConnUDP(network string, laddr, raddr *net.UDPAddr, cfg *Config) (errRet error) {
 	var c *net.UDPConn
@@ -316,6 +332,7 @@ func (cc *connUDPBase) initConnUDP(network string, laddr, raddr *net.UDPAddr, cf
 		}
 	}
 
+	//@ cfg.RevealIsLow()
 	//@ unfold cfg.Mem()
 	// Set and confirm send buffer size
 	if cfg.SendBufferSize != 0 {
@@ -414,12 +431,13 @@ func (c *connUDPBase) Write(b []byte /*@, ghost underlyingConn *net.UDPConn @*/)
 }
 
 // @ requires  acc(dst.Mem(), _)
-// @ preserves acc(c.Mem(), _)
+// @ preserves acc(c.Mem(), _) && c.IsLow(true)
 // @ preserves unfolding acc(c.Mem(), _) in c.conn == underlyingConn
 // @ preserves acc(sl.Bytes(b, 0, len(b)), R15)
 // @ ensures   err == nil ==> 0 <= n && n <= len(b)
 // @ ensures   err != nil ==> err.ErrorMem()
 func (c *connUDPBase) WriteTo(b []byte, dst *net.UDPAddr /*@, ghost underlyingConn *net.UDPConn @*/) (n int, err error) {
+	//@ c.RevealIsLow(true, R56, true)
 	//@ unfold acc(c.Mem(), _)
 	if c.Remote != nil {
 		return c.conn.Write(b)
@@ -445,10 +463,11 @@ func (c *connUDPBase) RemoteAddr() (u *net.UDPAddr) {
 	return c.Remote
 }
 
-// @ requires c.Mem()
+// @ requires c.Mem() && c.IsLow(true)
 // @ ensures  err != nil ==> err.ErrorMem()
 // @ decreases
 func (c *connUDPBase) Close() (err error) {
+	//@ c.RevealIsLow(false, writePerm, true)
 	//@ unfold c.Mem()
 	if c.closed {
 		return nil
@@ -459,23 +478,31 @@ func (c *connUDPBase) Close() (err error) {
 
 // NewReadMessages allocates memory for reading IPv4 Linux network stack
 // messages.
+// NOTE: The verification of this function is somewhat unstable.
+// Gobra issue #957 tracks this instability.
 // @ requires 0 < n
+// @ requires low(n)
 // @ ensures  len(res) == n
 // @ ensures  forall i int :: { &res[i] } 0 <= i && i < n ==> res[i].Mem() && res[i].GetAddr() == nil
 // @ decreases
 func NewReadMessages(n int) (res Messages) {
 	m := make(Messages, n)
-	//@ invariant forall j int :: { &m[j] } (0 <= j && j < i0) ==> m[j].Mem() && m[j].GetAddr() == nil
-	//@ invariant forall j int :: { &m[j] } (i0 <= j && j < len(m)) ==> acc(&m[j]) && m[j].N == 0
-	//@ invariant forall j int :: { m[j].Addr } (i0 <= j && j < len(m)) ==> m[j].Addr == nil
-	//@ invariant forall j int :: { m[j].OOB } (i0 <= j && j < len(m)) ==> m[j].OOB == nil
+	//@ invariant forall j int :: { &m[j] } (0 <= j && j < i0) ==> m[j].Mem()
+	//@ invariant forall j int :: { m[j].GetAddr() } (0 <= j && j < i0) ==> m[j].GetAddr() == nil
+	//@ invariant forall j int :: { &m[j] } (i0 <= j && j < len(m)) ==> acc(&m[j])
+	//@ invariant forall j int :: { &m[j].N } (i0 <= j && j < len(m)) ==> m[j].N == 0
+	//@ invariant forall j int :: { &m[j].Addr } (i0 <= j && j < len(m)) ==> m[j].Addr == nil
+	//@ invariant forall j int :: { &m[j].OOB } (i0 <= j && j < len(m)) ==> m[j].OOB == nil
+	//@ invariant low(i0)
 	//@ decreases len(m) - i
 	for i := range m /*@ with i0 @*/ {
 		// Allocate a single-element, to avoid allocations when setting the buffer.
 		m[i].Buffers = make([][]byte, 1)
 		//@ fold sl.Bytes(m[i].Buffers[0], 0, len(m[i].Buffers[0]))
 		//@ fold sl.Bytes(m[i].OOB, 0, len(m[i].OOB))
+		//@ BeforeFold:
 		//@ fold m[i].Mem()
+		//@ assert forall j int :: { m[j].GetAddr() } 0 <= j && j < i0 ==> old[BeforeFold](m[j].GetAddr()) == nil
 	}
 	return m
 }
diff --git a/private/underlay/conn/conn_spec.gobra b/private/underlay/conn/conn_spec.gobra
index 92fcef78f..909a23c0e 100644
--- a/private/underlay/conn/conn_spec.gobra
+++ b/private/underlay/conn/conn_spec.gobra
@@ -40,6 +40,63 @@ pred (c *connUDPBase) MemWithoutConn() {
 	(c.Remote != nil ==> acc(c.Remote.Mem(), _))
 }
 
+ghost
+requires  withConn ==> c.Mem()
+requires !withConn ==> c.MemWithoutConn()
+decreases
+pure func (c *connUDPBase) GetClosed(withConn bool) bool {
+	return withConn ? (
+		unfolding c.Mem() in c.closed) : (unfolding c.MemWithoutConn() in c.closed)
+}
+
+ghost
+requires  withConn ==> c.Mem()
+requires !withConn ==> c.MemWithoutConn()
+decreases
+pure func (c *connUDPBase) GetRemote(withConn bool) *net.UDPAddr {
+	return withConn ? (
+		unfolding c.Mem() in c.Remote) : (unfolding c.MemWithoutConn() in c.Remote)
+}
+
+// TODO: Once Gobra issue #846 is resolved, actually implement `IsLow`.
+ghost
+trusted
+requires  withConn ==> c.Mem()
+requires !withConn ==> c.MemWithoutConn()
+decreases
+pure func (c *connUDPBase) IsLow(withConn bool) bool
+
+// "Reveal the body" of `c.IsLow` (necessary bc. we can't implement `c.IsLow` yet).
+// TODO: Once Gobra issue #846 is resolved, implement this.
+ghost
+trusted
+requires p > 0
+requires  wildcard &&  withConn ==> acc(c.Mem(), _)
+requires  wildcard && !withConn ==> acc(c.MemWithoutConn(), _)
+requires !wildcard &&  withConn ==> acc(c.Mem(), p)
+requires !wildcard && !withConn ==> acc(c.MemWithoutConn(), p)
+requires c.IsLow(withConn)
+ensures   wildcard &&  withConn ==> acc(c.Mem(), _)
+ensures   wildcard && !withConn ==> acc(c.MemWithoutConn(), _)
+ensures  !wildcard &&  withConn ==> acc(c.Mem(), p)
+ensures  !wildcard && !withConn ==> acc(c.MemWithoutConn(), p)
+ensures  low(c.GetClosed(withConn)) && low(c.GetRemote(withConn) != nil)
+decreases
+func (c *connUDPBase) RevealIsLow(wildcard bool, p perm, withConn bool)
+
+// Assert `c.IsLow` (necessary bc. we can't implement `c.IsLow` yet).
+// TODO: Once Gobra issue #846 is resolved, implement this.
+ghost
+trusted
+requires  wildcard ==> acc(c.Mem(), _)
+requires !wildcard ==> acc(c.Mem(), R1)
+requires low(c.GetClosed(true)) && low(c.GetRemote(true) != nil)
+ensures   wildcard ==> acc(c.Mem(), _)
+ensures  !wildcard ==> acc(c.Mem(), R1)
+ensures  c.IsLow(true)
+decreases
+func (c *connUDPBase) AssertIsLow(wildcard bool)
+
 // Shown to be satisfiable in newConnUDPIPv4
 pred (c *connUDPIPv4) Mem() {
 	acc(&c.pconn) &&
@@ -48,6 +105,26 @@ pred (c *connUDPIPv4) Mem() {
 	c.pconn.GetUnderlyingConn() == (unfolding c.connUDPBase.MemWithoutConn() in c.conn)
 }
 
+// TODO: Once Gobra issue #846 is resolved, actually implement `IsLow`.
+ghost
+trusted
+requires c.Mem()
+decreases
+pure func (c *connUDPIPv4) IsLow() bool
+
+// "Reveal the body" of `c.IsLow` (necessary bc. we can't implement `c.IsLow` yet).
+// TODO: Once Gobra issue #846 is resolved, implement this.
+ghost
+trusted
+requires  wildcard ==> acc(c.Mem(), _)
+requires !wildcard ==> acc(c.Mem(), R1)
+requires c.IsLow()
+ensures   wildcard ==> acc(c.Mem(), _)
+ensures  !wildcard ==> acc(c.Mem(), R1)
+ensures  unfolding acc(c.Mem(), _) in c.connUDPBase.IsLow(false)
+decreases
+func (c *connUDPIPv4) RevealIsLow(wildcard bool)
+
 // Shown to be satisfiable in newConnUDPIPv6
 pred (c *connUDPIPv6) Mem() {
 	acc(&c.pconn) &&
@@ -56,12 +133,54 @@ pred (c *connUDPIPv6) Mem() {
 	c.pconn.GetUnderlyingConn() == (unfolding c.connUDPBase.MemWithoutConn() in c.conn)
 }
 
+// TODO: Once Gobra issue #846 is resolved, actually implement `IsLow`.
+ghost
+trusted
+requires c.Mem()
+decreases
+pure func (c *connUDPIPv6) IsLow() bool
+
+// "Reveal the body" of `c.IsLow` (necessary bc. we can't implement `c.IsLow` yet).
+// TODO: Once Gobra issue #846 is resolved, implement this.
+ghost
+trusted
+requires  wildcard ==> acc(c.Mem(), _)
+requires !wildcard ==> acc(c.Mem(), R1)
+requires c.IsLow()
+ensures   wildcard ==> acc(c.Mem(), _)
+ensures  !wildcard ==> acc(c.Mem(), R1)
+ensures  unfolding acc(c.Mem(), _) in c.connUDPBase.IsLow(false)
+decreases
+func (c *connUDPIPv6) RevealIsLow(wildcard bool)
+
 pred (c *Config) Mem() {
 	acc(c) &&
 	0 <= c.SendBufferSize &&
 	0 <= c.ReceiveBufferSize
 }
 
+requires c.Mem()
+decreases
+pure func (c *Config) Deref() Config {
+	return unfolding c.Mem() in *c
+}
+
+// TODO: Once Gobra issue #846 is resolved, actually implement `IsLow`.
+ghost
+trusted
+requires c.Mem()
+decreases
+pure func (c *Config) IsLow() bool
+
+// "Reveal the body" of `c.IsLow` (necessary bc. we can't implement `c.IsLow` yet).
+// TODO: Once Gobra issue #846 is resolved, implement this.
+ghost
+trusted
+requires acc(c.Mem(), R1) && c.IsLow()
+ensures  acc(c.Mem(), R1) && low(c.Deref())
+decreases
+func (c *Config) RevealIsLow()
+
 /** Lift methods in *connUDPBase to *connUDPIPv4 **/
 *connUDPIPv4 implements Conn
 
@@ -100,12 +219,14 @@ func (c *connUDPIPv4) Write(b []byte) (n int, err error) {
 }
 
 requires  acc(dst.Mem(), _)
-preserves acc(c.Mem(), _)
+preserves acc(c.Mem(), _) && c.IsLow()
 preserves acc(sl.Bytes(b, 0, len(b)), R15)
 ensures   err == nil ==> 0 <= n && n <= len(b)
 ensures   err != nil ==> err.ErrorMem()
 func (c *connUDPIPv4) WriteTo(b []byte, dst *net.UDPAddr) (n int, err error) {
+	c.RevealIsLow(true)
 	unfold acc(c.Mem(), _)
+	c.connUDPBase.RevealIsLow(true, R56, false)
 	unfold acc(c.connUDPBase.MemWithoutConn(), _)
 	assert c.pconn.GetUnderlyingConn() == c.conn
 	tmpImpl := c.conn
@@ -113,6 +234,7 @@ func (c *connUDPIPv4) WriteTo(b []byte, dst *net.UDPAddr) (n int, err error) {
 	var packetconn *ipv4.PacketConn = c.pconn
 	assert tmpItf == c.conn
 	fold acc(c.connUDPBase.Mem(), _)
+	c.connUDPBase.AssertIsLow(true)
 	n1, err1 := c.connUDPBase.WriteTo(b, dst, tmpImpl)
 	return n1, err1
 }
@@ -135,14 +257,17 @@ func (c *connUDPIPv4) RemoteAddr() (u *net.UDPAddr) {
 	return c.connUDPBase.RemoteAddr()
 }
 
-requires c.Mem()
+requires c.Mem() && c.IsLow()
 ensures  err != nil ==> err.ErrorMem()
 decreases
 func (c *connUDPIPv4) Close() (err error) {
+	c.RevealIsLow(false)
 	unfold c.Mem()
+	c.connUDPBase.RevealIsLow(false, R1, false)
 	unfold c.connUDPBase.MemWithoutConn()
 	c.pconn.ExchangePerm()
 	fold c.connUDPBase.Mem()
+	c.connUDPBase.AssertIsLow(false)
 	c.connUDPBase.Close()
 }
 /** End of Lift methods in *connUDPBase to *connUDPIPv4 **/
@@ -186,12 +311,14 @@ func (c *connUDPIPv6) Write(b []byte) (n int, err error) {
 }
 
 requires  acc(dst.Mem(), _)
-preserves acc(c.Mem(), _)
+preserves acc(c.Mem(), _) && c.IsLow()
 preserves acc(sl.Bytes(b, 0, len(b)), R15)
 ensures   err == nil ==> 0 <= n && n <= len(b)
 ensures   err != nil ==> err.ErrorMem()
 func (c *connUDPIPv6) WriteTo(b []byte, dst *net.UDPAddr) (n int, err error) {
+	c.RevealIsLow(true)
 	unfold acc(c.Mem(), _)
+	c.connUDPBase.RevealIsLow(true, R56, false)
 	unfold acc(c.connUDPBase.MemWithoutConn(), _)
 	assert c.pconn.GetUnderlyingConn() == c.conn
 	tmpImpl := c.conn
@@ -199,6 +326,7 @@ func (c *connUDPIPv6) WriteTo(b []byte, dst *net.UDPAddr) (n int, err error) {
 	var packetconn *ipv6.PacketConn = c.pconn
 	assert tmpItf == c.conn
 	fold acc(c.connUDPBase.Mem(), _)
+	c.connUDPBase.AssertIsLow(true)
 	n1, err1 := c.connUDPBase.WriteTo(b, dst, tmpImpl)
 	return n1, err1
 }
@@ -221,14 +349,17 @@ func (c *connUDPIPv6) RemoteAddr() (u *net.UDPAddr) {
 	return c.connUDPBase.RemoteAddr()
 }
 
-requires c.Mem()
+requires c.Mem() && c.IsLow()
 ensures  err != nil ==> err.ErrorMem()
 decreases
 func (c *connUDPIPv6) Close() (err error) {
+	c.RevealIsLow(false)
 	unfold c.Mem()
+	c.connUDPBase.RevealIsLow(false, R1, false)
 	unfold c.connUDPBase.MemWithoutConn()
 	c.pconn.ExchangePerm()
 	fold c.connUDPBase.Mem()
+	c.connUDPBase.AssertIsLow(false)
 	c.connUDPBase.Close()
 }
 /** End of Lift methods in *connUDPBase to *connUDPIPv6 **/
diff --git a/private/underlay/sockctrl/sockopt.go b/private/underlay/sockctrl/sockopt.go
index 3fdf7295a..cef94a8e5 100644
--- a/private/underlay/sockctrl/sockopt.go
+++ b/private/underlay/sockctrl/sockopt.go
@@ -21,10 +21,14 @@ import (
 	"syscall"
 )
 
-//@ trusted
-//@ preserves c.Mem()
-//@ ensures   e != nil ==> e.ErrorMem()
-//@ decreases _
+// As the implementation of `GetsockoptInt` is a bit involved, we (possibly)
+// overspecify this function to recover low(inputs) ==> low(outputs).
+// @ trusted
+// @ requires  low(level) && low(opt)
+// @ preserves c.Mem() && c.IsLow()
+// @ ensures   e != nil ==> e.ErrorMem()
+// @ ensures   low(r) && low(e != nil)
+// @ decreases _
 func GetsockoptInt(c *net.UDPConn, level, opt int) (r int, e error) {
 	var val int
 	err := SockControl(c, func(fd int) error {
@@ -35,10 +39,10 @@ func GetsockoptInt(c *net.UDPConn, level, opt int) (r int, e error) {
 	return val, err
 }
 
-//@ trusted
-//@ preserves c.Mem()
-//@ ensures   e != nil ==> e.ErrorMem()
-//@ decreases _
+// @ trusted
+// @ preserves c.Mem()
+// @ ensures   e != nil ==> e.ErrorMem()
+// @ decreases _
 func SetsockoptInt(c *net.UDPConn, level, opt, value int) (e error) {
 	return SockControl(c, func(fd int) error {
 		return syscall.SetsockoptInt(fd, level, opt, value)
diff --git a/router/dataplane.go b/router/dataplane.go
index a2539743a..430886ca7 100644
--- a/router/dataplane.go
+++ b/router/dataplane.go
@@ -148,6 +148,15 @@ type bfdSession interface {
 // with the same name in private/underlay/conn/Conn.
 type BatchConn interface {
 	// @ pred Mem()
+	
+	// Return whether all the underlying data that needs to be low for the
+	// computation of `WriteTo`, `Close` is low.
+	// We add this here to match the `Conn` interface in `private/underlay/conn`.
+	// TODO: Once Gobra issue #955 is resolved, mark as `hyper`.
+	// @ ghost
+	// @ requires Mem()
+	// @ decreases
+	// @ pure IsLow() bool
 
 	// @ requires  acc(Mem(), _)
 	// @ requires  forall i int :: { &msgs[i] } 0 <= i && i < len(msgs) ==>
@@ -176,9 +185,19 @@ type BatchConn interface {
 	// @ ensures   err == nil ==>
 	// @ 	forall i int :: { &msgs[i] } 0 <= i && i < n ==>
 	// @ 		MsgToAbsVal(&msgs[i], ingressID) == old(MultiReadBioIO_val(place, n)[i])
+	// Classification spec for SIF.
+	// The received messages are low, i.e., observable by the attacker.
+	// TODO: Once Gobra issue 846 is resolved, mark `msgs` as low instead of the
+	// abstraction, as `msgs` contains the data actually received and we don't
+	// necessarily have low(abstraction) ==> low(concrete).
+	// Expressing this without pure Boolean functions is rather tedious and not
+	// worth the time at the moment, IMO.
+	// @ ensures   err == nil ==>
+	// @ 	forall i int :: { MultiReadBioIO_val(place, n)[i] } 0 <= i && i < n ==>
+	// @		low(old(MultiReadBioIO_val(place, n)[i]))
 	ReadBatch(msgs underlayconn.Messages /*@, ghost ingressID uint16, ghost prophecyM int, ghost place io.Place @*/) (n int, err error)
 	// @ requires  acc(addr.Mem(), _)
-	// @ requires  acc(Mem(), _)
+	// @ requires  acc(Mem(), _) && IsLow()
 	// @ preserves acc(sl.Bytes(b, 0, len(b)), R10)
 	// @ ensures   err == nil ==> 0 <= n && n <= len(b)
 	// @ ensures   err != nil ==> err.ErrorMem()
@@ -192,6 +211,11 @@ type BatchConn interface {
 	// preconditions for IO-spec:
 	// @ requires  MsgToAbsVal(&msgs[0], egressID) == ioAbsPkts
 	// @ requires  io.token(place) && io.CBioIO_bio3s_send(place, ioAbsPkts)
+	// Classification spec for SIF.
+	// The messages to be sent need to be low, i.e., observable by the attacker.
+	// TODO: Once Gobra issue 846 is resolved, mark `msgs` as low instead of the
+	// abstraction. See comment on `ReadBatch` above for explanation.
+	// @ requires  low(ioAbsPkts)
 	// @ ensures   acc(msgs[0].Mem(), R50) && msgs[0].HasActiveAddr()
 	// @ ensures   acc(sl.Bytes(msgs[0].GetFstBuffer(), 0, len(msgs[0].GetFstBuffer())), R50)
 	// @ ensures   err == nil ==> 0 <= n && n <= len(msgs)
@@ -201,7 +225,7 @@ type BatchConn interface {
 	// otherwise the router cannot continue after failing to send a packet.
 	// @ ensures   io.token(old(io.dp3s_iospec_bio3s_send_T(place, ioAbsPkts)))
 	WriteBatch(msgs underlayconn.Messages, flags int /*@, ghost egressID uint16, ghost place io.Place, ghost ioAbsPkts io.Val @*/) (n int, err error)
-	// @ requires Mem()
+	// @ requires Mem() && IsLow()
 	// @ ensures  err != nil ==> err.ErrorMem()
 	// @ decreases
 	Close() (err error)
diff --git a/router/io-spec-atomic-events.gobra b/router/io-spec-atomic-events.gobra
index 13f0a781c..ce10cd648 100644
--- a/router/io-spec-atomic-events.gobra
+++ b/router/io-spec-atomic-events.gobra
@@ -27,6 +27,7 @@ import (
 	"sync"
 	io "verification/io"
 	gsync "verification/utils/ghost_sync"
+	"github.com/scionproto/scion/pkg/slayers/path"
 )
 
 ghost
@@ -155,6 +156,35 @@ func AtomicXover(oldPkt io.Pkt, ingressID option[io.Ifs], newPkt io.Pkt, egressI
 	UpdateElemWitness(s.obuf, ioSharedArg.OBufY, egressID, newPkt)
 	ghost *ioSharedArg.State = io.dp3s_add_obuf(s, egressID, newPkt)
 	ghost *ioSharedArg.Place = tN
+	fold SharedInv!< dp, ioSharedArg !>()
+	ghost ioLock.Unlock()
+}
+
+ghost
+requires  low(beta) && low(ts) && low(inif) && low(egif)
+requires  path.AbsMac(sigma) == io.nextMsgtermSpec(dp.Asid(), inif, egif, ts, beta)
+preserves acc(ioLock.LockP(), _)
+preserves ioLock.LockInv() == SharedInv!< dp, ioSharedArg !>
+ensures   forall i int :: { sigma[i] } 0 <= i && i < len(sigma) ==> low(sigma[i])
+decreases _
+func AtomicDecl(beta set[io.MsgTerm], ts uint, inif, egif option[io.Ifs], sigma [path.MacLen]byte, ioLock gpointer[gsync.GhostMutex], ioSharedArg SharedArg, dp io.DataPlaneSpec) {
+	ghost ioLock.Lock()
+	unfold SharedInv!< dp, ioSharedArg !>()
+
+	t, s := *ioSharedArg.Place, *ioSharedArg.State
+	ghost decl_val := io.Val(io.IO_decl_val{beta, ts, inif, egif, sigma})
+
+	// TODO: Remove this assumption
+	assume path.AbsMac(sigma) == io.AbsMac(sigma)
+	assert dp.dp4s_iospec_bio4s_decl_guard(s, t, decl_val)
+	unfold dp.dp3s_iospec_ordered(s, t)
+	unfold dp.dp4s_iospec_bio4s_decl(s, t)
+
+	io.TriggerBodyIoDecl(decl_val)
+	tN := io.dp4s_iospec_bio4s_decl_T(t, decl_val)
+	io.Decl(t, decl_val)
+	ghost *ioSharedArg.Place = tN
+
 	fold SharedInv!< dp, ioSharedArg !>()
 	ghost ioLock.Unlock()
 }
\ No newline at end of file
diff --git a/verification/dependencies/encoding/encoding.gobra b/verification/dependencies/encoding/encoding.gobra
index 8c5947e25..9818da569 100644
--- a/verification/dependencies/encoding/encoding.gobra
+++ b/verification/dependencies/encoding/encoding.gobra
@@ -19,7 +19,11 @@ package encoding
 type TextUnmarshaler interface {
 	pred Mem()
 	
-	preserves Mem() && acc(text)
+	requires  acc(text)
+	requires  low(len(text)) && forall i int :: { text[i] } 0 <= i && i < len(text) &&
+		low(i) ==> low(text[i])
+	preserves Mem()
+	ensures   acc(text)
 	decreases
 	UnmarshalText(text []byte) error
 }
diff --git a/verification/dependencies/flag/flag.gobra b/verification/dependencies/flag/flag.gobra
index d8c640a58..1fb4ccfb8 100644
--- a/verification/dependencies/flag/flag.gobra
+++ b/verification/dependencies/flag/flag.gobra
@@ -19,11 +19,12 @@ package flag
 type Value interface {
 	pred Mem()
 
-	preserves acc(Mem())
+	preserves Mem()
 	decreases
 	String() string
 
-	preserves acc(Mem())
+	requires  low(s)
+	preserves Mem()
 	decreases
-	Set(string) error
+	Set(s string) error
 }
diff --git a/verification/dependencies/fmt/fmt.gobra b/verification/dependencies/fmt/fmt.gobra
index eefea525f..4f08a2715 100644
--- a/verification/dependencies/fmt/fmt.gobra
+++ b/verification/dependencies/fmt/fmt.gobra
@@ -28,7 +28,7 @@ func Sprintf(format string, v ...interface{}) string
 type Stringer interface {
 	pred Mem()
 
-	preserves acc(Mem())
+	preserves Mem()
 	decreases
 	String() string
 }
diff --git a/verification/dependencies/net/ip.gobra b/verification/dependencies/net/ip.gobra
index fac00c253..bfac564a7 100644
--- a/verification/dependencies/net/ip.gobra
+++ b/verification/dependencies/net/ip.gobra
@@ -61,8 +61,12 @@ preserves forall i int :: { &ip[i] } 0 <= i && i < len(ip) ==> acc(&ip[i], R15)
 func (ip IP) IsGlobalUnicast() bool
 
 // To4 converts the IPv4 address ip to a 4-byte representation.
-preserves wildcard ==> forall i int :: { &ip[i] } 0 <= i && i < len(ip) ==> acc(&ip[i], _)
-preserves !wildcard ==> forall i int :: { &ip[i] } 0 <= i && i < len(ip) ==> acc(&ip[i], R20)
+requires   wildcard ==> forall i int :: { &ip[i] } 0 <= i && i < len(ip) ==> acc(&ip[i], _)
+requires  !wildcard ==> forall i int :: { &ip[i] } 0 <= i && i < len(ip) ==> acc(&ip[i], R20)
+requires  low(len(ip)) && forall i int :: { &ip[i] } 0 <= i && i < len(ip) &&
+	low(i) ==> low(ip[i])
+ensures    wildcard ==> forall i int :: { &ip[i] } 0 <= i && i < len(ip) ==> acc(&ip[i], _)
+ensures   !wildcard ==> forall i int :: { &ip[i] } 0 <= i && i < len(ip) ==> acc(&ip[i], R20)
 ensures   res != nil ==> len(res) == IPv4len
 ensures   len(ip) == IPv4len ==> ip === res
 ensures   (len(ip) == IPv6len && isZeros(ip[0:10]) && ip[10] == 255 && ip[11] == 255) ==> res != nil
@@ -74,11 +78,16 @@ ensures   (len(ip) == IPv6len && res != nil) ==>
 	let _ := sl.AssertSliceOverlap(ip, 12, 16) in
 	res === ip[12:16]
 ensures   len(ip) != IPv4len && len(ip) != IPv6len ==> res == nil
+ensures   low(res != nil)
 decreases
 func (ip IP) To4(ghost wildcard bool) (res IP) {
 	if len(ip) == IPv4len {
 		return ip
 	}
+	// This assertion is necessary to infer `low(isZeros(ip[0:10]))`.
+	assert len(ip) == IPv6len ==>
+		low(ip[0]) && low(ip[1]) && low(ip[2]) && low(ip[3]) && low(ip[4]) && 
+		low(ip[5]) && low(ip[6]) && low(ip[7]) && low(ip[8]) && low(ip[9])
 	if len(ip) == IPv6len &&
 		isZeros(ip[0:10]) &&
 		ip[10] == 255 &&
@@ -88,11 +97,20 @@ func (ip IP) To4(ghost wildcard bool) (res IP) {
 	return nil
 }
 
+ghost
 requires forall i int :: { &s[i] } 0 <= i && i < len(s) ==> acc(&s[i])
 decreases
-pure func isZeros(s []byte) bool
+pure func isZerosSpec(s []byte) bool {
+	return forall i int :: { &s[i] } 0 <= i && i < len(s) ==> s[i] == 0
+}
+
+requires forall i int :: { &s[i] } 0 <= i && i < len(s) ==> acc(&s[i])
+ensures  res == isZerosSpec(s)
+decreases
+pure func isZeros(s []byte) (res bool)
 
 // To16 converts the IP address ip to a 16-byte representation.
+requires  low(len(ip))
 preserves forall i int :: { &ip[i] } 0 <= i && i < len(ip) ==> acc(&ip[i], R15)
 ensures len(ip) == IPv4len ==>
 	(len(res) == IPv4len &&
@@ -143,5 +161,7 @@ pure func (ip IP) Equal(x IP) bool
 // ParseIP parses s as an IP address, returning the result.
 ensures forall i int :: {&res[i]} 0 <= i && i < len(res) ==> acc(&res[i])
 ensures res != nil ==> len(res) == IPv4len || len(res) == IPv6len
+ensures low(s) ==> low(res == nil) && low(len(res)) && 
+	forall i int :: { &res[i] } 0 <= i && i < len(res) && low(i) ==> low(res[i])
 decreases _
 func ParseIP(s string) (res IP)
diff --git a/verification/dependencies/net/udpsock.gobra b/verification/dependencies/net/udpsock.gobra
index d1a9f2b71..7c579863b 100644
--- a/verification/dependencies/net/udpsock.gobra
+++ b/verification/dependencies/net/udpsock.gobra
@@ -27,6 +27,40 @@ pred (a *UDPAddr) Mem() {
 	acc(a, R5) && sl.Bytes(a.IP, 0, len(a.IP))
 }
 
+requires a.Mem()
+decreases
+pure func (a *UDPAddr) GetIP() IP {
+	return unfolding a.Mem() in a.IP
+}
+
+requires a.Mem() && 0 <= i && i < len(a.GetIP())
+decreases
+pure func (a *UDPAddr) GetIPByte(i int) byte {
+	return unfolding a.Mem() in sl.GetByte(a.IP, 0, len(a.IP), i)
+}
+
+// TODO: Once Gobra issue #846 is resolved, actually implement `IsLow`.
+// - Here, `IsLow` will need to cover all fields (of `UDPAddr`), since we use 
+//   this information in `DialUDP` and `ListenUDP` to imply that all fields of 
+//   the resulting `UDPConn` object are low. 
+ghost
+trusted
+requires a.Mem()
+decreases
+pure func (a *UDPAddr) IsLow() bool
+
+// "Reveal the body" of `a.IsLow` (necessary bc. we can't implement `a.IsLow` yet).
+// TODO: Once Gobra issue #846 is resolved, implement this.
+ghost
+trusted
+requires acc(a.Mem(), R15) && a.IsLow()
+ensures  acc(a.Mem(), R15)
+ensures  low(len(a.GetIP()))
+ensures  forall i int :: { a.GetIPByte(i) } 0 <= i && i < len(a.GetIP()) ==>
+	low(i) ==> low(a.GetIPByte(i))
+decreases
+func (a *UDPAddr) RevealIsLow()
+
 (*UDPAddr) implements Addr {
 	(e *UDPAddr) Network() string {
 		return e.Network()
@@ -56,6 +90,14 @@ pred (u *UDPConn) Mem() {
 	acc(u)
 }
 
+// TODO: Once Gobra issue #846 is resolved, mark as `hyper`.
+// We assume that `IsLow` covers all fields of `UDPConn`, since we use this
+// information in `private/underlay/sockctrl/sockopt.go`, `GetsocketoptInt`
+ghost
+requires c.Mem()
+decreases
+pure func (c *UDPConn) IsLow() bool
+
 // ReadFromUDP acts like ReadFrom but returns a UDPAddr.
 preserves acc(c.Mem(), _)
 preserves sl.Bytes(b, 0, len(b))
@@ -113,24 +155,32 @@ decreases
 func (c *UDPConn) Close() (err error)
 
 requires acc(laddr.Mem(), _)
-ensures  err == nil ==> conn.Mem()
+requires low(network) && laddr.IsLow()
+ensures  err == nil ==> conn.Mem() && conn.IsLow()
 ensures  err != nil ==> err.ErrorMem()
+ensures  low(err != nil)
 decreases _
 func ListenUDP(network string, laddr *UDPAddr) (conn *UDPConn, err error)
 
 requires acc(laddr.Mem(), _)
 requires acc(raddr.Mem(), _)
-ensures  err == nil ==> conn.Mem()
+requires low(network) && laddr.IsLow() && raddr.IsLow()
+ensures  err == nil ==> conn.Mem() && conn.IsLow()
 ensures  err != nil ==> err.ErrorMem()
+ensures  low(err != nil)
 decreases _
 func DialUDP(network string, laddr, raddr *UDPAddr) (conn *UDPConn, err error)
 
-preserves c.Mem()
+requires  low(bytes)
+preserves c.Mem() && c.IsLow()
 ensures   err != nil ==> err.ErrorMem()
+ensures   low(err != nil)
 decreases _
 func (c *UDPConn) SetWriteBuffer(bytes int) (err error)
 
-preserves c.Mem()
+requires  low(bytes)
+preserves c.Mem() && c.IsLow()
+ensures   low(err != nil)
 ensures   err != nil ==> err.ErrorMem()
 decreases _
 func (c *UDPConn) SetReadBuffer(bytes int) (err error)
diff --git a/verification/dependencies/strconv/atoi.gobra b/verification/dependencies/strconv/atoi.gobra
index 26ee30282..9b035db1d 100644
--- a/verification/dependencies/strconv/atoi.gobra
+++ b/verification/dependencies/strconv/atoi.gobra
@@ -39,6 +39,7 @@ requires base == 0 || (2 <= base && base <= 36)
 requires bitSize > 0 && bitSize <= 64
 ensures retErr == nil ==> (ret >= 0 && ret < Exp(2, bitSize))
 ensures retErr != nil ==> retErr.ErrorMem()
+ensures (low(s) && low(base) && low(bitSize)) ==> (low(ret) && low(retErr))
 decreases _
 func ParseUint(s string, base int, bitSize int) (ret uint64, retErr error)
 
diff --git a/verification/dependencies/strconv/itoa.gobra b/verification/dependencies/strconv/itoa.gobra
index 4f478ed1a..db86ef46b 100644
--- a/verification/dependencies/strconv/itoa.gobra
+++ b/verification/dependencies/strconv/itoa.gobra
@@ -16,8 +16,9 @@ const fastSmalls = true // enable fast path for small integers
 // for digit values >= 10.
 requires i >= 0
 requires 2 <= base && base <= 36
+ensures low(i) && low(base) ==> low(res)
 decreases
-func FormatUint(i uint64, base int) string
+func FormatUint(i uint64, base int) (res string)
 
 // FormatInt returns the string representation of i in the given base,
 // for 2 <= base <= 36. The result uses the lower-case letters 'a' to 'z'
diff --git a/verification/dependencies/strings/strings.gobra b/verification/dependencies/strings/strings.gobra
index 521896b3e..68324344a 100644
--- a/verification/dependencies/strings/strings.gobra
+++ b/verification/dependencies/strings/strings.gobra
@@ -66,7 +66,9 @@ func SplitAfterN(s, sep string, n int) (res []string)
 
 // Split slices s into all substrings separated by sep and returns a slice of
 // the substrings between those separators.
-ensures forall i int :: { &res[i] } 0 <= i && i < len(res) ==> acc(&res[i])
+ensures forall i int :: { &res[i] } 0 <= i && i < len(res) ==> 
+	acc(&res[i]) && ((low(s) && low(sep)) ==> low(i) ==> low(res[i]))
+ensures (low(s) && low(sep)) ==> low(len(res))
 decreases _
 func Split(s, sep string) (res []string) //{ return genSplit(s, sep, 0, -1) }
 
@@ -111,8 +113,9 @@ decreases _
 func ToUpper(s string) string
 
 // ToLower returns s with all Unicode letters mapped to their lower case.
+ensures low(s) ==> low(res)
 decreases _
-func ToLower(s string) string
+func ToLower(s string) (res string)
 
 // ToTitle returns a copy of the string s with all Unicode letters mapped to
 // their Unicode title case.
@@ -156,8 +159,9 @@ func TrimPrefix(s, prefix string) string
 
 // TrimSuffix returns s without the provided trailing suffix string.
 // If s doesn't end with suffix, s is returned unchanged.
+ensures low(s) && low(suffix) ==> low(res)
 decreases _
-func TrimSuffix(s, suffix string) string
+func TrimSuffix(s, suffix string) (res string)
 
 // Replace returns a copy of the string s with the first n
 // non-overlapping instances of old replaced by new.
diff --git a/verification/io/io-spec.gobra b/verification/io/io-spec.gobra
index 55a1b782e..b4ad4bd4c 100644
--- a/verification/io/io-spec.gobra
+++ b/verification/io/io-spec.gobra
@@ -33,7 +33,8 @@ pred (dp DataPlaneSpec) dp3s_iospec_ordered(s Dp3sStateLocal, t Place) {
 	dp.dp3s_iospec_bio3s_send(s, t) &&
 	dp.dp3s_iospec_bio3s_recv(s, t) &&
 	dp.dp3s_iospec_skip(s, t) &&
-	dp.dp3s_iospec_stop(s, t)
+	dp.dp3s_iospec_stop(s, t) &&
+	dp.dp4s_iospec_bio4s_decl(s, t)  // SIF
 }
 
 type Place int
@@ -299,6 +300,49 @@ pred (dp DataPlaneSpec) dp3s_iospec_stop(s Dp3sStateLocal, t Place) {
 	true
 }
 
+// Declassification specification for SIF.
+// Members whose id start with "dp4s" correspond to additions to the IO spec
+// related to SIF.
+pred CBio_IN_bio4s_decl(t Place, v Val)
+
+ghost
+decreases
+pure func dp4s_iospec_bio4s_decl_T(t Place, v Val) Place
+
+ghost
+requires v.isIO_decl_val
+decreases
+pure func (dp DataPlaneSpec) dp4s_iospec_bio4s_decl_guard(s Dp3sStateLocal, t Place, v Val) bool {
+	// Cf. `router.gobra`, in particular `hf_valid`.
+	// NOTE: Formatting this differently leads to a parsing error.
+	return AbsMac(v.IO_decl_val_sigma) == (nextMsgtermSpec(
+		dp.Asid(),
+		v.IO_decl_val_inif,
+		v.IO_decl_val_egif,
+		v.IO_decl_val_ts,
+		v.IO_decl_val_beta))
+}
+
+pred (dp DataPlaneSpec) dp4s_iospec_bio4s_decl(s Dp3sStateLocal, t Place) {
+	// NOTE: Formatting this differently leads to a parsing error.
+	forall v Val :: { TriggerBodyIoDecl(v) } (
+		match v {
+			case IO_decl_val{?beta, ?ts, ?inif, ?egif, ?sigma}:
+				let _ignored := TriggerBodyIoDecl(v) in
+				(dp.dp4s_iospec_bio4s_decl_guard(s, t, v) ==>
+					(CBio_IN_bio4s_decl(t, v) &&
+					dp.dp3s_iospec_ordered(
+						s,
+						dp4s_iospec_bio4s_decl_T(t, v))))
+			default:
+				true
+		})
+}
+
+ghost
+decreases
+pure func TriggerBodyIoDecl(v Val) BogusTrigger { return BogusTrigger{} }
+
 /** BIO operations **/
 ghost
 decreases
@@ -318,4 +362,15 @@ requires token(t) && CBio_IN_bio3s_exit(t, v)
 ensures  token(old(dp3s_iospec_bio3s_exit_T(t, v)))
 func Exit(ghost t Place, ghost v Val)
 
-/** End of helper functions to perfrom BIO operations **/
+ghost
+decreases
+requires token(t) && CBio_IN_bio4s_decl(t, v)
+requires v.isIO_decl_val &&
+ 	low(v.IO_decl_val_inif) && low(v.IO_decl_val_egif) &&
+ 	low(v.IO_decl_val_ts) && low(v.IO_decl_val_beta)
+ensures  token(dp4s_iospec_bio4s_decl_T(t, v))
+ensures  forall i int :: { v.IO_decl_val_sigma[i] } 0 <= i && i < len(v.IO_decl_val_sigma) ==> 
+	low(v.IO_decl_val_sigma[i])
+func Decl(ghost t Place, ghost v Val)
+
+/** End of helper functions to perform BIO operations **/
diff --git a/verification/io/tmp_defs.gobra b/verification/io/tmp_defs.gobra
new file mode 100644
index 000000000..c6b54fd69
--- /dev/null
+++ b/verification/io/tmp_defs.gobra
@@ -0,0 +1,11 @@
+// +gobra
+
+package io
+
+// TODO: Remove this and link with actual definitions in "io_msgterm_spec.gobra"
+
+const MacLen = 6
+
+ghost
+decreases
+pure func AbsMac(mac [MacLen]byte) MsgTerm
\ No newline at end of file
diff --git a/verification/io/values.gobra b/verification/io/values.gobra
index 2d42801af..288cb3068 100644
--- a/verification/io/values.gobra
+++ b/verification/io/values.gobra
@@ -52,4 +52,23 @@ ghost type Val adt {
 		ValInternal2_2 Pkt
 		ValInternal2_3 Ifs
 	}
+
+	// Output (to env.) for declassification action (SIF).
+	// The actual value to declassify is the hop authenticator (MAC tag) `sigma`;
+	// the other values act as the "tag" p to make the allowed declassifications
+	// deterministic in the low data (i.e., to make the IOD spec well-defined;
+	// see "Verifiable Security Policies for Distributed Systems" by Wolf et al.).
+	// `beta` is a segment identifier, `ts` a timestamp, and `inif` and `egif`
+	// the ingress and egress interfaces (resp.).
+	// See `hf_valid`, for why we need these values in particular.
+	// TODO: We might want to use the concrete instead of the abstract values for p.
+	IO_decl_val {
+		IO_decl_val_beta set[MsgTerm]  // uinfo
+		IO_decl_val_ts uint
+		IO_decl_val_inif option[Ifs]
+		IO_decl_val_egif option[Ifs]
+		// TODO: Relate to `path.MacLen`
+		IO_decl_val_sigma [MacLen]byte
+	}
+
 }
\ No newline at end of file
diff --git a/verification/utils/sif/assumptions.gobra b/verification/utils/sif/assumptions.gobra
new file mode 100644
index 000000000..c0cd79938
--- /dev/null
+++ b/verification/utils/sif/assumptions.gobra
@@ -0,0 +1,11 @@
+// +gobra
+
+package sif
+
+// TODO: Once Gobra issue #832 is resolved, introduce body and prove this.
+ghost
+requires p > 0 && acc(b, p)
+requires low(len(b)) && forall i int :: { &b[i] } 0 <= i && i < len(b) && low(i) ==> low(b[i])
+ensures  acc(b, p) && low(string(b))
+decreases
+func LowSliceImpliesLowString(b []byte, p perm)