From a0f41c8103b679daa165a2416a8fe407c4a3f75e Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paris.fr>
Date: Thu, 26 Oct 2023 13:46:10 +0200
Subject: [PATCH] Adding getkey and host function in toproverif translation
---
src/main/java/avatartranslator/AvatarMethod.java | 2 ++
.../java/avatartranslator/toproverif/AVATAR2ProVerif.java | 8 ++++++++
2 files changed, 10 insertions(+)
diff --git a/src/main/java/avatartranslator/AvatarMethod.java b/src/main/java/avatartranslator/AvatarMethod.java
index b1900492db..fa39ff3239 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 37d4306e57..6dd9171ebe 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
--
GitLab