diff --git a/README.md b/README.md
index a1c68552b..07834b485 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
 # VerifiedSCION
 
-This package contains the **verified** implementation of the
+This package contains the **verified** implementation of the router from the
 [SCION](http://www.scion-architecture.net) protocol, a future Internet architecture.
 SCION is the first
 clean-slate Internet architecture designed to provide route control, failure
@@ -10,7 +10,7 @@ isolation, and explicit trust information for end-to-end communication.
 
 To find out more about the project, please visit the [official project page](https://www.pm.inf.ethz.ch/research/verifiedscion.html).
 
-> We are currently in the process of migrating the specifications and other annotations from the [original VerifiedSCION repository](https://github.com/jcp19/VerifiedSCION) to this one. This repository contains an up-to-date version of SCION (which we plan to keep updated), as well as improvements resulting from our experience from our first efforts on verifying SCION.
+> This repository contains a recent version of SCION (which we plan to keep updated), as well as fixes to the bugs we report as a result of verifying the SCION router from the mainline SCION repository.
 
 ## Methodology
 We focus on verifying the main implementation of SCION, written in the *Go* programming language.
diff --git a/verification/dependencies/github.com/google/gopacket/base.gobra b/verification/dependencies/github.com/google/gopacket/base.gobra
index 6a55f340e..9c0ae5c81 100644
--- a/verification/dependencies/github.com/google/gopacket/base.gobra
+++ b/verification/dependencies/github.com/google/gopacket/base.gobra
@@ -60,8 +60,8 @@ ensures   len(res) != 0 ==> res === ub[start:end]
 decreases
 func (p Payload) Payload(ghost ub []byte) (res []byte, ghost start int, ghost end int) {
 	res = []byte(p)
-    assert unfolding acc(p.Mem(ub), R20) in true
-    return res, 0, len(p)
+	assert unfolding acc(p.Mem(ub), R20) in true
+	return res, 0, len(p)
 }
 
 requires b != nil && b.Mem()
diff --git a/verification/io/dataplane_abstract.gobra b/verification/io/dataplane_abstract.gobra
index ba717326a..e78c901e9 100644
--- a/verification/io/dataplane_abstract.gobra
+++ b/verification/io/dataplane_abstract.gobra
@@ -21,16 +21,16 @@ package io
 //     to the interface y of AS a2.
 type DataPlaneSpec adt {
 	DataPlaneSpec_{
-		linkTypes		dict[IO_ifs]IO_Link
-		neighborIAs		dict[IO_ifs]IO_as
-		localIA			IO_as
-		links			dict[AsIfsPair]AsIfsPair
+		linkTypes   dict[IO_ifs]IO_Link
+		neighborIAs dict[IO_ifs]IO_as
+		localIA     IO_as
+		links       dict[AsIfsPair]AsIfsPair
 	}
 }
 
 type AsIfsPair struct {
-	asid	IO_as
-	ifs		IO_ifs
+	asid IO_as
+	ifs  IO_ifs
 }
 
 ghost
diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra
index a5c48ccae..7f600a457 100644
--- a/verification/io/other_defs.gobra
+++ b/verification/io/other_defs.gobra
@@ -200,6 +200,7 @@ type IO_dp2_state adt {
 }
 
 ghost
+opaque
 decreases
 pure func (m IO_msgterm) extract_asid() IO_as {
 	return m.MsgTerm_Hash_.MsgTerm_MPair_1.MsgTerm_Key_.Key_macK_
diff --git a/verification/io/router.gobra b/verification/io/router.gobra
index f1741bed5..533bdee8d 100644
--- a/verification/io/router.gobra
+++ b/verification/io/router.gobra
@@ -27,47 +27,72 @@ pure func if2term(ifs option[IO_ifs]) IO_msgterm {
 		case none[IO_ifs]:
 			MsgTerm_Empty{}
 		default:
-			IO_msgterm(MsgTerm_AS{IO_as(get(ifs))})
+			MsgTerm_AS{IO_as(get(ifs))}
 	}
 }
 
 ghost
 decreases
 pure func (dp DataPlaneSpec) hf_valid(d bool, ts uint, uinfo set[IO_msgterm], hf IO_HF) bool {
+	return hf_valid_impl(dp.Asid(), ts, uinfo, hf)
+}
+
+ghost
+decreases
+pure func hf_valid_impl(asid IO_as, ts uint, uinfo set[IO_msgterm], hf IO_HF) bool {
 	return let inif := hf.InIF2 in
 		let egif := hf.EgIF2 in
-		let x := hf.HVF in
-		let l := IO_msgterm(MsgTerm_L{
-			seq[IO_msgterm]{
-				IO_msgterm(MsgTerm_Num{ts}),
-				if2term(inif),
-				if2term(egif),
-				IO_msgterm(MsgTerm_FS{uinfo})}}) in
-		x == mac(macKey(asidToKey(dp.Asid())), l)
+		let hvf := hf.HVF in
+		let next := nextMsgtermSpec(asid, inif, egif, ts, uinfo) in
+		hvf == next
+}
+
+ghost
+opaque
+ensures result.extract_asid() == asid
+decreases
+pure func nextMsgtermSpec(asid IO_as, inif option[IO_ifs], egif option[IO_ifs], ts uint, uinfo set[IO_msgterm]) (result IO_msgterm) {
+	return let l := plaintextToMac(inif, egif, ts, uinfo) in
+		let res := mac(macKey(asidToKey(asid)), l) in
+		let _ := reveal res.extract_asid() in
+		res
+}
+
+ghost
+decreases
+pure func plaintextToMac(inif option[IO_ifs], egif option[IO_ifs], ts uint, uinfo set[IO_msgterm]) IO_msgterm {
+	return MsgTerm_L {
+		seq[IO_msgterm]{
+			MsgTerm_Num{ts},
+			if2term(inif),
+			if2term(egif),
+			MsgTerm_FS{uinfo},
+		},
+	}
 }
 
 ghost
 decreases
 pure func macKey(key IO_key) IO_msgterm {
-	return IO_msgterm(MsgTerm_Key{key})
+	return MsgTerm_Key{key}
 }
 
 ghost
 decreases
 pure func mac(fst IO_msgterm, snd IO_msgterm) IO_msgterm {
-	return IO_msgterm( MsgTerm_Hash {
-		MsgTerm_Hash_ : IO_msgterm( MsgTerm_MPair{
-			MsgTerm_MPair_1 : fst,
-			MsgTerm_MPair_2 : snd,
-		}),
-	})
+	return MsgTerm_Hash {
+		MsgTerm_Hash_: MsgTerm_MPair {
+			MsgTerm_MPair_1: fst,
+			MsgTerm_MPair_2: snd,
+		},
+	}
 }
 
 // helper function, not defined in IO spec
 ghost
 decreases
-pure func asidToKey(asid IO_as) IO_key{
-	return IO_key(Key_macK{asid})
+pure func asidToKey(asid IO_as) IO_key {
+	return Key_macK{asid}
 }
 
 ghost