diff --git a/pkg/slayers/scion.go b/pkg/slayers/scion.go
index e3de3e8f3..bc3c7d7b1 100644
--- a/pkg/slayers/scion.go
+++ b/pkg/slayers/scion.go
@@ -223,12 +223,8 @@ func (s *SCION) NetworkFlow() (res gopacket.Flow) {
 // @ ensures   acc(s.Mem(ubuf), R0)
 // @ ensures   sl.Bytes(ubuf, 0, len(ubuf))
 // @ ensures   sl.Bytes(b.UBuf(), 0, len(b.UBuf()))
-// TODO: hide internal spec details
 // @ ensures   e == nil && s.HasOneHopPath(ubuf) ==>
-// @	len(b.UBuf()) == old(len(b.UBuf())) + unfolding acc(s.Mem(ubuf), R55) in
-// @		(CmnHdrLen + s.AddrHdrLenSpecInternal() + s.Path.LenSpec(ubuf[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen]))
-// @ ensures   e == nil && s.HasOneHopPath(ubuf) ==>
-// @	(unfolding acc(s.Mem(ubuf), R55) in CmnHdrLen + s.AddrHdrLenSpecInternal() + s.Path.LenSpec(ubuf[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen])) <= len(ubuf)
+// @ 	len(b.UBuf()) == old(len(b.UBuf())) + s.MinimalSizeOfUbuf(ubuf)
 // @ ensures   e != nil ==> e.ErrorMem()
 // post for IO:
 // @ ensures   e == nil && old(s.EqPathType(ubuf)) ==>
diff --git a/pkg/slayers/scion_spec.gobra b/pkg/slayers/scion_spec.gobra
index a66bce011..4b446e946 100644
--- a/pkg/slayers/scion_spec.gobra
+++ b/pkg/slayers/scion_spec.gobra
@@ -762,6 +762,32 @@ pure func (s *SCION) HasOneHopPath(ghost ub []byte) bool {
 	return unfolding acc(s.Mem(ub), _) in typeOf(s.Path) == type[*onehop.Path]
 }
 
+ghost
+requires acc(&s.DstAddrType, _) &&
+	acc(&s.SrcAddrType, _)      &&
+	acc(&s.HdrLen, _)           &&
+	acc(&s.Path, _)
+requires s.DstAddrType.Has3Bits() && s.SrcAddrType.Has3Bits()
+requires 0 <= CmnHdrLen+s.AddrHdrLenSpecInternal() &&
+	CmnHdrLen+s.AddrHdrLenSpecInternal() <= s.HdrLen*LineLen &&
+	s.HdrLen*LineLen <= len(ub)
+requires s.Path != nil
+requires acc(s.Path.Mem(ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen]), _)
+decreases
+pure func (s *SCION) MinimalSizeOfUbufWithOneHopOpenInv(ub []byte) int {
+	return let pathSlice := ub[CmnHdrLen+s.AddrHdrLenSpecInternal() : s.HdrLen*LineLen] in
+		let pathLen := s.Path.LenSpec(pathSlice) in
+		CmnHdrLen + s.AddrHdrLenSpecInternal() + pathLen
+}
+
+ghost
+requires acc(s.Mem(ub), _)
+decreases
+pure func (s *SCION) MinimalSizeOfUbuf(ub []byte) int {
+	return unfolding acc(s.Mem(ub), _) in
+		s.MinimalSizeOfUbufWithOneHopOpenInv(ub)
+}
+
 ghost
 requires acc(s.Mem(ub), _)
 requires s.HasOneHopPath(ub)