extends responder implementation to interop with initiator, bug fixes

Author: ArquintL

dh/implementation/initiator/initiator.go

@@ -408,10 +408,10 @@ func (i *Initiator) ProduceHsMsg3() (signedMsg3 []byte, err error) {
 			i.irKey, i.riKey = NewBytes(32), NewBytes(32)
 			//@ sharedSecretB := Abs(sharedSecret)
 			err = KDF2Slice(i.irKey, i.riKey, sharedSecret /*@, sharedSecretB @*/)
-			/*@
-			ghost if err == nil {
-				fold HandshakeCompletedPred(i.irKey, i.riKey, i.xT, i.YT)
-			} @*/
+			if err == nil {
+				i.l.PrintKeys(i.irKey, i.riKey)
+				//@ fold HandshakeCompletedPred(i.irKey, i.riKey, i.xT, i.YT)
+			}
 		}
 	//@ )
 

dh/implementation/library/io.go

@@ -30,3 +30,10 @@ func NewError(msg string) (err error) {
 func (l *LibState) PrintSharedSecret(sharedSecret []byte) {
 	fmt.Printf("Initiator & responder agreed on shared secret %x\n", sharedSecret)
 }
+
+//@ trusted
+//@ preserves acc(l.Mem(), 1/16)
+//@ preserves acc(Mem(irKey), 1/16) && acc(Mem(riKey), 1/16)
+func (l *LibState) PrintKeys(irKey, riKey []byte) {
+	fmt.Printf("IR Key %x\nRI Key %x\n", irKey, riKey)
+}

dh/implementation/library/marshal.go

@@ -95,7 +95,7 @@ func (l *LibState) MarshalMsg3(msg3 *Msg3) (res []byte, err error) {
 //@ ensures err == nil ==> Mem(res)
 //@ ensures err == nil ==> Abs(res) == by.tuple2B(by.integer32B(TransMsgTag), Abs(ciphertext))
 func (l *LibState) MarshalTransportMsg(ciphertext []byte) (res []byte, err error) {
-	res = make([]byte, len(ciphertext) + 4)
+	res = make([]byte, 4)
 	binary.BigEndian.PutUint32(res[:4], TransMsgTag)
 	return append(res, ciphertext...), nil
 }

dh/implementation/main.go

@@ -2,26 +2,30 @@ package main
 
 import "bufio"
 import "encoding/base64"
+import "errors"
 import "flag"
 import "fmt"
 import "os"
 import "dh-gobra/initiator"
 import "dh-gobra/iolib"
 
 type Config struct {
+	IsInitiator            bool
 	PrivateKey             string
 	PeerEndpoint           string // <address>:<port>, e.g. "127.0.0.1:57654" (IPv4) or "[::1]:57950" (IPv6)
 	PeerPublicKey          string
 }
 
 func parseArgs() Config {
+	isInitiatorPtr := flag.Bool("isInitiator", false, "specifies whether this instance should act as an initiator")
 	privateKeyPtr := flag.String("privateKey", "", "base64 encoded private key of this protocol participant")
 	peerEndpointPtr := flag.String("endpoint", "", "<address>:<port> of the peer's endpoint")
 	peerPublicKeyPtr := flag.String("peerPublicKey", "", "base64 encoded public key of the peer")
 
 	flag.Parse()
 
 	config := Config{
+		IsInitiator:            *isInitiatorPtr,
 		PrivateKey:             *privateKeyPtr,
 		PeerEndpoint:           *peerEndpointPtr,
 		PeerPublicKey:          *peerPublicKeyPtr,
@@ -33,97 +37,94 @@ func main() {
 	// parse args
 	config := parseArgs()
 
+	if !config.IsInitiator {
+		reportAndExit(errors.New("responder is currently not implemented"))
+	}
+
 	privateKey, peerPublicKey, err := parseKeys(config)
 	if err != nil {
-		os.Exit(-1)
-		return
+		reportAndExit(err)
 	}
 
 	initiator, err := initiator.NewInitiator(privateKey, peerPublicKey)
 	if err != nil {
-		os.Exit(-1)
-		return
+		reportAndExit(err)
 	}
 
 	iolib, err := iolib.NewLibState(config.PeerEndpoint)
 	if err != nil {
-		os.Exit(-1)
-		return
+		reportAndExit(err)
 	}
 
 	hsMsg1, err := initiator.ProduceHsMsg1()
 	if err != nil {
-		os.Exit(-1)
-		return
+		reportAndExit(err)
 	}
 
 	err = iolib.Send(hsMsg1)
 	if err != nil {
-		os.Exit(-1)
-		return
+		reportAndExit(err)
 	}
 
 	hsMsg2, err := iolib.Recv()
 	if err != nil {
-		os.Exit(-1)
-		return
+		reportAndExit(err)
 	}
 
 	err = initiator.ProcessHsMsg2(hsMsg2)
 	if err != nil {
-		os.Exit(-1)
-		return
+		reportAndExit(err)
 	}
 
 	hsMsg3, err := initiator.ProduceHsMsg3()
 	if err != nil {
-		os.Exit(-1)
-		return
+		reportAndExit(err)
 	}
 
 	err = iolib.Send(hsMsg3)
 	if err != nil {
-		os.Exit(-1)
-		return
+		reportAndExit(err)
 	}
 
 	// handshake is now over
 	scanner := bufio.NewScanner(os.Stdin)
+	fmt.Println("Enter a payload to be sent:")
 	for scanner.Scan() {
 		line := scanner.Text()
 		requestMsg, err := initiator.ProduceTransportMsg([]byte(line))
 		if err != nil {
-			os.Exit(-1)
-			return
+			reportAndExit(err)
 		}
 		err = iolib.Send(requestMsg)
 		if err != nil {
-			os.Exit(-1)
-			return
+			reportAndExit(err)
 		}
 
 		responseMsg, err := iolib.Recv()
 		if err != nil {
-			os.Exit(-1)
-			return
+			reportAndExit(err)
 		}
 		responsePayload, err := initiator.ProcessTransportMsg(responseMsg)
 		if err != nil {
-			os.Exit(-1)
-			return
+			reportAndExit(err)
 		}
-		fmt.Println(responsePayload)
+		fmt.Printf("Received: %s\n", string(responsePayload))
+		fmt.Println("Enter a payload to be sent:")
 	}
 
 	iolib.Close()
 	if err == nil {
 		os.Exit(0)
 	} else {
-		fmt.Println(err)
-		os.Exit(1)
+		reportAndExit(err)
 	}
 }
 
+func reportAndExit(err error) {
+	fmt.Println(err)
+	os.Exit(1)
+}
+
 func parseKeys(config Config) (privateKey [64]byte, peerPublicKey [32]byte, err error) {
 	encoding := base64.StdEncoding
 	privateKeySlice, err := encoding.DecodeString(config.PrivateKey)

dh/implementation/responder/README.md

@@ -11,6 +11,10 @@ Build:
 ```
 gradle build
 ```
+The following command explicitly specifies a JDK in case the default one is too old:
+```
+gradle build -Dorg.gradle.java.home=/opt/homebrew/opt/openjdk
+```
 
 Run:
 ```

dh/implementation/responder/build.gradle

@@ -23,7 +23,7 @@ jar {
         attributes 'Main-Class': mainClassName
     }
     // name of the generated JAR output:
-    baseName 'dh-gobra'
+    archiveBaseName.set('dh-gobra')
     // to create a fat JAR:
     from {
         configurations.runtimeClasspath.collect { it.isDirectory() ? it : zipTree(it) }
@@ -39,6 +39,6 @@ jar {
 
 // set destination for JAR output:
 tasks.withType(Jar) {
-    destinationDir = file("$rootDir")
+    destinationDirectory = file("$rootDir")
     // duplicatesStrategy = DuplicatesStrategy.EXCLUDE
 }

dh/implementation/responder/src/main/java/dhgobra/library/Library.java

@@ -4,11 +4,14 @@
 import java.util.Arrays;
 import java.util.Random;
 import java.net.*;
+import java.nio.ByteBuffer;
 import java.security.KeyFactory;
 import java.security.NoSuchAlgorithmException;
+import java.security.InvalidAlgorithmParameterException;
 import java.security.InvalidKeyException;
 import java.security.PublicKey;
 import java.security.PrivateKey;
+import java.security.SecureRandom;
 import java.security.Signature;
 import java.security.SignatureException;
 import java.security.spec.EdECPoint;
@@ -17,9 +20,16 @@
 import java.security.spec.NamedParameterSpec;
 import java.security.spec.EdECPrivateKeySpec;
 import java.security.spec.PKCS8EncodedKeySpec;
-import javax.crypto.spec.SecretKeySpec;
 import java.security.spec.X509EncodedKeySpec;
 import java.io.IOException;
+import java.util.Scanner;
+import javax.crypto.Cipher;
+import javax.crypto.BadPaddingException;
+import javax.crypto.IllegalBlockSizeException;
+import javax.crypto.NoSuchPaddingException;
+import javax.crypto.SecretKey;
+import javax.crypto.spec.IvParameterSpec;
+import javax.crypto.spec.SecretKeySpec;
 // import org.bouncycastle.crypto.params.Ed25519PublicKeyParameters;
 // import org.bouncycastle.crypto.Signer;
 // import org.bouncycastle.crypto.signers.Ed25519Signer;
@@ -329,7 +339,7 @@ private boolean longInRange(long value) {
         return true;
     }
 
-    private byte[] uint32ToBytes(long value) {
+    public byte[] uint32ToBytes(long value) {
         if (!longInRange(value)) {
             return null;
         }
@@ -341,7 +351,7 @@ private byte[] uint32ToBytes(long value) {
         };
     }
 
-    private long bytesToUint32(byte[] data) {
+    public long bytesToUint32(byte[] data) {
         if (data == null || data.length != 4) {
             return -1;
         }
@@ -359,4 +369,79 @@ public void notMatchY() {
     public void success(byte[] sharedSecret) {
         System.out.println("Initiator & responder agreed on shared secret " + convertToHex(sharedSecret));
     }
+
+    private static final String ENCRYPT_ALGO = "ChaCha20-Poly1305";
+    private static final int NONCE_LEN = 12;
+    public byte[] encrypt(byte[] plaintext, byte[] key) {
+        Cipher cipher;
+        try {
+            cipher = Cipher.getInstance(ENCRYPT_ALGO);
+        } catch (NoSuchAlgorithmException | NoSuchPaddingException e) {
+            return null;
+        }
+
+        byte[] nonce = new byte[NONCE_LEN];
+        new SecureRandom().nextBytes(nonce);
+
+        // IV, initialization value with nonce
+        IvParameterSpec iv = new IvParameterSpec(nonce);
+
+        SecretKey keyObject = new SecretKeySpec(key, "AES");
+        try {
+            cipher.init(Cipher.ENCRYPT_MODE, keyObject, iv);
+        } catch (InvalidKeyException | InvalidAlgorithmParameterException e) {
+            return null;
+        }
+
+        byte[] encryptedText;
+        try {
+            encryptedText = cipher.doFinal(plaintext);
+        } catch (IllegalBlockSizeException | BadPaddingException e) {
+            return null;
+        }
+
+        // prepend nonce to the encrypted text
+        byte[] output = ByteBuffer.allocate(encryptedText.length + NONCE_LEN)
+                .put(nonce)
+                .put(encryptedText)
+                .array();
+
+        return output;
+    }
+
+    public byte[] decrypt(byte[] ciphertext, byte[] key) {
+        ByteBuffer bb = ByteBuffer.wrap(ciphertext);
+
+        // split ciphertext to get the prepended nonce
+        byte[] nonce = new byte[NONCE_LEN];
+        byte[] encryptedText = new byte[ciphertext.length - NONCE_LEN];
+        bb.get(nonce);
+        bb.get(encryptedText);
+        
+        Cipher cipher;
+        try {
+            cipher = Cipher.getInstance(ENCRYPT_ALGO);
+        } catch (NoSuchAlgorithmException | NoSuchPaddingException e) {
+            System.out.println(e);
+            return null;
+        }
+
+        IvParameterSpec iv = new IvParameterSpec(nonce);
+
+        SecretKey keyObject = new SecretKeySpec(key, "AES");
+        try {
+            cipher.init(Cipher.DECRYPT_MODE, keyObject, iv);
+        } catch (InvalidKeyException | InvalidAlgorithmParameterException e) {
+            System.out.println(e);
+            return null;
+        }
+
+        // decrypted text
+        try {
+            return cipher.doFinal(encryptedText);
+        } catch (IllegalBlockSizeException | BadPaddingException e) {
+            System.out.println(e);
+            return null;
+        }
+    }
 }