diff --git a/verification/io/other_defs.gobra b/verification/io/other_defs.gobra
index 70c390daf..269e41626 100644
--- a/verification/io/other_defs.gobra
+++ b/verification/io/other_defs.gobra
@@ -48,7 +48,7 @@ type IO_msgterm adt {
 	}
 
 	MsgTerm_Num {
-		MsgTerm_Num_ int // formallized as nat in Isabelle
+		MsgTerm_Num_ uint // formallized as nat in Isabelle
 	}
 
 	MsgTerm_Key {
@@ -60,7 +60,7 @@ type IO_msgterm adt {
 	}
 
 	MsgTerm_FS {
-		MsgTerm_FS_ seq[IO_msgterm]
+		MsgTerm_FS_ set[IO_msgterm]
 	}
 
 	MsgTerm_MPair {
@@ -107,8 +107,6 @@ pure func (hf IO_HF) extr_asid() IO_as {
 	return hf.HVF.extract_asid()
 }
 
-
-
 // function 'toab' in Isabelle, originally of type HF_scheme -> aahi_scheme
 ghost
 pure
@@ -159,31 +157,46 @@ pure func link_type(p1 IO_as, p2 IO_ifs) IO_Link
 
 ghost
 decreases
-pure func egif_prov2(hf1 IO_HF, asid IO_as) bool
+pure func egif_prov2(hf1 IO_HF, asid IO_as) bool{
+	return egif2_type(hf1, asid, IO_Link(IO_CustProv{}))
+}
 
 ghost
 decreases
-pure func egif_core2(hf1 IO_HF, asid IO_as) bool
+pure func egif_core2(hf1 IO_HF, asid IO_as) bool{
+	return egif2_type(hf1, asid, IO_Link(IO_PeerOrCore{}))
+}
 
 ghost
 decreases
-pure func egif_cust2(hf1 IO_HF, asid IO_as) bool
+pure func egif_cust2(hf1 IO_HF, asid IO_as) bool{
+	return egif2_type(hf1, asid, IO_Link(IO_ProvCust{}))
+}
 
 ghost
 decreases
-pure func inif_cust2(hf1 IO_HF, asid IO_as) bool
+pure func inif_cust2(hf1 IO_HF, asid IO_as) bool{
+	return inif2_type(hf1, asid, IO_Link(IO_ProvCust{}))
+}
 
 ghost
 decreases
-pure func inif_core2(hf1 IO_HF, asid IO_as) bool
+pure func inif_core2(hf1 IO_HF, asid IO_as) bool{
+	return inif2_type(hf1, asid, IO_Link(IO_PeerOrCore{}))
+}
 
 ghost
 decreases
-pure func inif_prov2(hf1 IO_HF, asid IO_as) bool
+pure func inif_prov2(hf1 IO_HF, asid IO_as) bool{
+	return inif2_type(hf1, asid, IO_Link(IO_CustProv{}))
+}
 
 ghost
 decreases
-pure func if_type(asid IO_as, ifs option[IO_ifs], link IO_Link) bool
+pure func if_type(asid IO_as, ifs option[IO_ifs], link IO_Link) bool{
+	return ifs == none[IO_ifs] ? false : link_type(asid, get(ifs)) == link
+	//exists outif IO_ifs :: some(outif) == ifs && link_type(asid, outif) == link
+}
 
 type ext2_rec struct {
 	op1 IO_as
@@ -213,10 +226,9 @@ ghost
 decreases
 pure func dp2_in_ext(s IO_dp2_state, asid IO_as, ifs IO_ifs, pkt IO_pkt2) bool
 
-// TODO: how is this defined?
-// extract_asid
 ghost
 decreases
-pure func (m IO_msgterm) extract_asid() IO_as
-
+pure func (m IO_msgterm) extract_asid() IO_as {
+	return m.MsgTerm_Hash_.MsgTerm_MPair_1.MsgTerm_Key_.Key_macK_
+}
 /* End of To clarify */
diff --git a/verification/io/router.gobra b/verification/io/router.gobra
index 0bad5df67..d4ea683c8 100644
--- a/verification/io/router.gobra
+++ b/verification/io/router.gobra
@@ -27,11 +27,52 @@ pure func core_as_set() set[IO_as]
 
 ghost
 decreases
-pure func hf_valid(p1 bool, p2 uint, p3 set[IO_msgterm], p4 IO_HF) bool
+pure func hf_valid(p1 bool, p2 uint, p3 set[IO_msgterm], p4 IO_HF) bool {
+	return let inif := p4.InIF2 in
+		let egif := p4.EgIF2 in
+		let x := p4.HVF in
+		let ts := IO_msgterm(MsgTerm_Num{p2}) in 
+		let uinfo := IO_msgterm(MsgTerm_FS{p3}) in
+		let l := IO_msgterm(MsgTerm_L{seq[IO_msgterm]{ts, if2term(inif), if2term(egif), uinfo}}) in 
+		exists a IO_key :: x == mac(macKey(a), l)
+}
+
+//Helper function (not in Isabelle)
+ghost
+decreases
+pure func asidToKey(asid IO_as) IO_key{
+	return IO_key(Key_macK{asid})
+}
+
+ghost
+decreases
+pure func macKey(key IO_key) IO_msgterm {
+	return IO_msgterm(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, 
+		}),
+	})
+}
+
+ghost 
+decreases
+pure func if2term(ifs option[IO_ifs]) IO_msgterm {
+	return ifs == none[IO_ifs] ? MsgTerm_Empty{} : IO_msgterm(MsgTerm_AS{IO_as(get(ifs))})
+}
 
 ghost
 decreases
-pure func upd_uinfo(p1 set[IO_msgterm], p2 IO_HF) set[IO_msgterm]
+pure func upd_uinfo(p1 set[IO_msgterm], p2 IO_HF) set[IO_msgterm] {
+	return let setHVF := set[IO_msgterm]{p2.HVF} in
+		(p1 union setHVF) setminus (p1 intersection setHVF)
+}
 
 ghost
 decreases