updates WireGuard oracle to Python3, updates Dockerfile such that it builds again

Author: ArquintL

tamarin-docker/Dockerfile

@@ -1,35 +1,37 @@
-# the image for verifying the Tamarin model is based on Python2 because `wireguard.oracle`
-# is a Python file that has to be executed with Python2.
-FROM python:2.7
+FROM debian:bookworm-slim@sha256:df52e55e3361a81ac1bead266f3373ee55d29aa50cf0975d440c2be3483d8ed3
+# note that trixie does not have `libtinfo5` anymore (but `libtinfo6` which doesn't work with the current Maude version)
 
 RUN apt-get update && \
     apt-get install -y \
         curl \
-        zip \
-        locales \
-        graphviz \
         # libtinfo5 is needed by maude
-        libtinfo5
+        libtinfo5 \
+        locales \
+        # we need python for our Tamarin oracle:
+        python3 \
+        # vim is only provided for convenience:
+        vim \
+        wget \
+        zip \
+        make \
+        git    
 
 # `/.local/bin` is the installation location of Tamarin and its dependencies
 RUN mkdir -p /.local/bin
 ENV PATH=/.local/bin:$PATH
 
-# install Haskell stack
-RUN curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C /.local/bin '*/stack' && \
-    chmod a+x /.local/bin/stack && \
-    stack --no-terminal setup
-
 # install Maude
-ENV TAMARIN_VERSION 1.6.0
-ENV MAUDE_URL https://github.com/tamarin-prover/tamarin-prover/releases/download/$TAMARIN_VERSION/Maude-2.7.1-linux.zip
+ENV TAMARIN_RELEASE_VERSION_FOR_MAUDE="1.6.0"
+ENV MAUDE_VERSION="2.7.1"
+ENV MAUDE_URL="https://github.com/tamarin-prover/tamarin-prover/releases/download/$TAMARIN_RELEASE_VERSION_FOR_MAUDE/Maude-$MAUDE_VERSION-linux.zip"
 RUN curl -q -s -S -L --create-dirs -o maude.zip $MAUDE_URL && \
     unzip maude.zip -d /.local/bin/ && \
     rm maude.zip && \
     mv /.local/bin/maude.linux64 /.local/bin/maude && \
     chmod a+x /.local/bin/maude
 
 # install tamarin-prover
+ENV TAMARIN_VERSION="1.10.0"
 RUN curl -q -s -S -L --create-dirs -o tamarin.tar.gz https://github.com/tamarin-prover/tamarin-prover/releases/download/$TAMARIN_VERSION/tamarin-prover-$TAMARIN_VERSION-linux64-ubuntu.tar.gz && \
     tar -x -C /.local/bin/ -f tamarin.tar.gz && \
     rm tamarin.tar.gz && \
@@ -39,9 +41,9 @@ RUN curl -q -s -S -L --create-dirs -o tamarin.tar.gz https://github.com/tamarin-
 USER root
 RUN sed -i '/en_US.UTF-8/s/^# //g' /etc/locale.gen && \
     locale-gen
-ENV LANG en_US.UTF-8  
-ENV LANGUAGE en_US:en  
-ENV LC_ALL en_US.UTF-8
+ENV LANG="en_US.UTF-8"
+ENV LANGUAGE="en_US:en"
+ENV LC_ALL="en_US.UTF-8"
 
 WORKDIR /tamarin
 COPY dh/model/dh.spthy .

wireguard/model/wireguard.oracle

@@ -1,9 +1,7 @@
-#!/usr/bin/python2
+#!/usr/bin/python3
 
 import re
-import os
 import sys
-debug = True
 
 lines = sys.stdin.readlines()
 lemma = sys.argv[1]
@@ -17,7 +15,7 @@ lemma = sys.argv[1]
 
 rank = []             # list of list of goals, main list is ordered by priority
 maxPrio = 110
-for i in range(0,maxPrio):
+for i in range(0, maxPrio):
   rank.append([])
 
 # SOURCES LEMMAS
@@ -39,5 +37,4 @@ else:
 for listGoals in reversed(rank):
   for goal in listGoals:
     sys.stderr.write(goal)
-    print goal
-
+    print(goal)