diff --git a/src/main/java/avatartranslator/AvatarMethod.java b/src/main/java/avatartranslator/AvatarMethod.java
index b1900492db4e649f95c07974706cab873c7f93f7..fa39ff3239bf1111c17fef97ac146f5f82f604cf 100644
--- a/src/main/java/avatartranslator/AvatarMethod.java
+++ b/src/main/java/avatartranslator/AvatarMethod.java
@@ -67,6 +67,8 @@ public class AvatarMethod extends AvatarElement implements NameChecker.NameStart
             "Message hash(Message msg)",
             "Message MAC(Message msg, Key k)",
             "bool verifyMAC(Message msg, Key k, Message macmsg)",
+            "Message host(Key k)",
+            "Key getKey(Message msg)",
             "Message concat2(Message msg1, Message msg2)",
             "Message concat3(Message msg1, Message msg2, Message msg3)",
             "Message concat4(Message msg1, Message msg2, Message msg3, Message msg4)",
diff --git a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
index 37d4306e57fbb3823751a85d77825b0d3e157df8..6dd9171ebefbbbacaa3d51ac10aed5262eece530 100755
--- a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -72,6 +72,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
     private final static String TRUE = "TRUE";
     private final static String FALSE = "FALSE";
     private final static String PK_PK = "pk";
+    private final static String HOST = "host";
+    private final static String GETKEY = "getKey";
     private final static String PK_ENCRYPT = "aencrypt";
     private final static String PK_DECRYPT = "adecrypt";
     private final static String PK_SIGN = "sign";
@@ -513,6 +515,12 @@ public class AVATAR2ProVerif implements AvatarTranslator {
         this.spec.addDeclaration(new ProVerifComment("HASH"));
         this.spec.addDeclaration(new ProVerifFunc(HASH_HASH, new String[]{"bitstring"}, "bitstring"));
 
+        this.spec.addDeclaration(new ProVerifComment("Key and host"));
+        this.spec.addDeclaration(new ProVerifFunc(HOST, new String[]{"bitstring"}, "bitstring"));
+        this.spec.addDeclaration(new ProVerifReduc(new ProVerifVar[]{new ProVerifVar("x", "bitstring")}, GETKEY + " (" + HOST + " (x)) = " +
+                "x"));
+
+
         this.spec.addDeclaration(new ProVerifComment("Channel"));
         this.spec.addDeclaration(new ProVerifVar(CH_MAINCH, "channel"));
         // TODO: add one encryption function per signal