diff --git a/BouncyCastle-JCA/src/DHParameterSpec.crysl b/BouncyCastle-JCA/src/DHParameterSpec.crysl
index 6225595..397efb0 100644
--- a/BouncyCastle-JCA/src/DHParameterSpec.crysl
+++ b/BouncyCastle-JCA/src/DHParameterSpec.crysl
@@ -1,22 +1,21 @@
 SPEC javax.crypto.spec.DHParameterSpec
 
-OBJECTS 
+OBJECTS
 	java.math.BigInteger p;
 	java.math.BigInteger g;
 	int l;
-	
+
 EVENTS
 	c1: DHParameterSpec(p, g);
 	c2: DHParameterSpec(p, g, l);
 	Con := c1 | c2;
-	
+
 ORDER
 	Con
 
 CONSTRAINTS
-	p >= 1^2048;
-	g >= 1^2048; 
-	
+	bitlength(p) >= 3000;// Choose an element g ∈ F∗ p withord(g) primeandq := ord(g) ≥ 2^250
+	bitlength(g) >= 250;
+
 ENSURES
 	preparedDH[this];
-	
\ No newline at end of file
diff --git a/BouncyCastle-JCA/src/GCMParameterSpec.crysl b/BouncyCastle-JCA/src/GCMParameterSpec.crysl
index 05815af..b4cbd12 100644
--- a/BouncyCastle-JCA/src/GCMParameterSpec.crysl
+++ b/BouncyCastle-JCA/src/GCMParameterSpec.crysl
@@ -5,6 +5,7 @@ OBJECTS
 	byte[] src;
 	int offset;
 	int len;
+	byte[] iv;
 	
 EVENTS
 	c1: GCMParameterSpec(tagLen, src);
@@ -15,10 +16,12 @@ ORDER
 	Con
 	
 CONSTRAINTS
-	tagLen in {96, 104, 112, 120, 128};
+	tagLen in {96, 104, 112, 120, 128};//GCM with a length of the GCM tags of at least 96 bits should be used.
 	length[src] >= offset + len;
 	offset >= 0;
 	len > 0;
+	length[iv] == 12;
+	unique[iv] // initiallization vector should not be repeated over the entire lifetime of a key
 	
 REQUIRES
 	randomized[src];
diff --git a/BouncyCastle-JCA/src/IvParameterSpec.crysl b/BouncyCastle-JCA/src/IvParameterSpec.crysl
index 00ae5c0..8e5881a 100644
--- a/BouncyCastle-JCA/src/IvParameterSpec.crysl
+++ b/BouncyCastle-JCA/src/IvParameterSpec.crysl
@@ -17,6 +17,7 @@ CONSTRAINTS
 	length[iv] >= offset + len;
 	offset >= 0;
 	len > 0;
+	unique[iv]
 	
 REQUIRES
 	randomized[iv];
diff --git a/BouncyCastle-JCA/src/KeyAgreement.crysl b/BouncyCastle-JCA/src/KeyAgreement.crysl
index 512efe2..94cb9c9 100644
--- a/BouncyCastle-JCA/src/KeyAgreement.crysl
+++ b/BouncyCastle-JCA/src/KeyAgreement.crysl
@@ -37,15 +37,19 @@ ORDER
 	Get, Init, DoPhase, (GenSecret | GenSecretBuffer)
 	
 CONSTRAINTS
-	algorithm in {"DH", "DiffieHellman", "NH" ,"ECDH", "ECDHC"};
+	algorithm in {"DH","DiffieHellman","ECDH","NH", "ECDHC"};
+	keyLength>=3000;
+	curveBits>= 250;
 	symmetricKeyAlgorithm in {"AES", "HmacSHA256", "HmacSHA384", "HmacSHA512",
 			 "HMACSHA3-256", "HMACSHA3-384", "HMACSHA3-512"};
+	tagLength>=96
+
 	
 REQUIRES
 	randomized[random];
 	generatedPrivkey[privKey];
 	generatedPubkey[pubKey];
-	algorithm in {"DiffieHellman", "DH"} => preparedDH[params];
+	algorithm in {"DiffieHellman","DH"} => preparedDH[params];
 	algorithm in {"ECDH", "ECDHC"} => preparedEC[params];
     
 ENSURES 
diff --git a/BouncyCastle-JCA/src/KeyGenerator.crysl b/BouncyCastle-JCA/src/KeyGenerator.crysl
index 67341cd..ecdad5b 100644
--- a/BouncyCastle-JCA/src/KeyGenerator.crysl
+++ b/BouncyCastle-JCA/src/KeyGenerator.crysl
@@ -32,7 +32,7 @@ CONSTRAINTS
 				"Twofish", "Poly1305-Twofish", "XSalsa20"};
 	algorithm in {"AES", "Poly1305-Camellia", "Camellia", "ChaCha", "Salsa20", "SHACAL-2", "Shacal2",
 				"Rijndael", "Serpent", "Tnepres", "ChaCha7539", "Poly1305", "Poly1305-Serpent", 
-				"Twofish", "Poly1305-Twofish", "XSalsa20"} => keysize in {128, 192, 256};
+				"Twofish", "Poly1305-Twofish", "XSalsa20"} => keysize >= 128;
 
 REQUIRES
 	randomized[random];
diff --git a/BouncyCastle-JCA/src/KeyPairGenerator.crysl b/BouncyCastle-JCA/src/KeyPairGenerator.crysl
index 163a890..d828b0a 100644
--- a/BouncyCastle-JCA/src/KeyPairGenerator.crysl
+++ b/BouncyCastle-JCA/src/KeyPairGenerator.crysl
@@ -15,7 +15,8 @@ EVENTS
 	i2: initialize(keysize, _);
 	i3: initialize(params);
 	i4: initialize(params, _);
-	Init := i1 | i2 | i3 | i4;
+	i5: initialize(java.security.spec.AlgorithmParameterSpec, java.security.SecureRandom)
+	Init := i1 | i2 | i3 | i4 | i5;
 
 	k1: keyPair = generateKeyPair();
 	k2: keyPair = genKeyPair();
@@ -25,18 +26,18 @@ ORDER
 	Get, Init, Gen
 
 CONSTRAINTS
-	algorithm in {"RSA", "DSA", "DiffieHellman", "DH", "EC", "ECDSA", "ECDH", "ECDHWITHSHA1KDF", "ECDHC", 
+	algorithm in {"RSA", "DSA", "DiffieHellman", "DH", "EC", "ECDSA", "ECDH", "ECDHWITHSHA1KDF", "ECDHC",
 			"ECIES", "ElGamal", "McElieceKobaraImai", "McEliecePointcheval", "McElieceFujisaki", 
 			"McEliece", "McEliece-CCA2", "NH", "QTESLA", "Rainbow", "SPHINCS256", "XMSS", "XMSSMT"};
 						
-	algorithm in {"RSA"} => keysize in {4096, 3072}; //BSI TR-02102-1 Recommends atleast 3000bits for keys
-	algorithm in {"DSA"} => keysize in {3072};
-	algorithm in {"DiffieHellman", "DH"} => keysize in {3072};
-	algorithm in {"EC", "ECDSA", "ECDH", "ECDHWITHSHA1KDF", "ECDHC", "ECIES"} => keysize in {256};
-	
+	algorithm in {"RSA"} => keysize >= 3000; //BSI TR-02102-1 Recommends atleast 3000bits for keys
+	algorithm in {"DSA"} => keysize >= 3072;
+	algorithm in {"DiffieHellman", "DH"} => keysize >= 3000;
+	algorithm in {"EC", "ECDSA", "ECDH", "ECDHWITHSHA1KDF", "ECDHC", "ECIES"} => keysize >= 320;
+	algorithm in {"DSA"} && afterYear >= 2029 => false;//# DSA deprecated after 2029
+
 REQUIRES
-	algorithm in {"RSA"} => preparedRSA[params];
-	algorithm in {"DSA"} => preparedDSA[params];
+    algorithm in {"RSA"} => preparedRSA[params];	algorithm in {"DSA"} => preparedDSA[params];
 	algorithm in {"DiffieHellman", "DH"} => preparedDH[params];
 	algorithm in {"EC"} => preparedEC[params];
 
diff --git a/BouncyCastle-JCA/src/RSAKeyGenParameterSpec.crysl b/BouncyCastle-JCA/src/RSAKeyGenParameterSpec.crysl
index d357e50..3e66bf8 100644
--- a/BouncyCastle-JCA/src/RSAKeyGenParameterSpec.crysl
+++ b/BouncyCastle-JCA/src/RSAKeyGenParameterSpec.crysl
@@ -12,7 +12,7 @@ ORDER
 	Con
 	
 CONSTRAINTS
-	keysize in {4096}; //BSI TR-02102-1 Recommends atleast 3000bits for keys
+	keysize >= 3000; //BSI TR-02102-1 Recommends atleast 3000bits for keys
 	publicExponent in {65537};
 	 
 ENSURES
diff --git a/BouncyCastle-JCA/src/SecureRandom.crysl b/BouncyCastle-JCA/src/SecureRandom.crysl
index 027ebee..a5e3a93 100644
--- a/BouncyCastle-JCA/src/SecureRandom.crysl
+++ b/BouncyCastle-JCA/src/SecureRandom.crysl
@@ -40,6 +40,8 @@ ORDER
  	
 CONSTRAINTS
 	algorithm in {"DEFAULT", "NONCEANDIV"};
+
+
 	
 REQUIRES	
 	randomized[seed];
diff --git a/BouncyCastle-JCA/src/Signature.crysl b/BouncyCastle-JCA/src/Signature.crysl
index 4d72bde..e688984 100644
--- a/BouncyCastle-JCA/src/Signature.crysl
+++ b/BouncyCastle-JCA/src/Signature.crysl
@@ -47,7 +47,7 @@ ORDER
 CONSTRAINTS
 	algorithm in {"ECDDSA", "SHA256WITHECDDSA", "SHA384WITHECDDSA", "SHA512WITHECDDSA", "SHA3-256WITHECDDSA", "SHA3-384WITHECDDSA", 
 			"SHA3-512WITHECDDSA", "SHA256WITHECNR", "SHA384WITHECNR", "SHA512WITHECNR", "SHA256withECDSA", "SHA256withDSA", 
-			 "SHA384withRSA", "SHA512withRSA", "SHA256withRSA", "SHA384withDSA", "SHA512withDSA", 
+			 "SHA384withRSA", "SHA512withRSA", "SHA256withRSA", "SHA384withDSA", "SHA512withDSA",
 			"QTESLA"};
 	length[input] >= offset + len;
     offset >= 0;
diff --git a/BouncyCastle/src/PaddedBufferedBlockCipher.crysl b/BouncyCastle/src/PaddedBufferedBlockCipher.crysl
index b4e7d6b..b6d8cee 100644
--- a/BouncyCastle/src/PaddedBufferedBlockCipher.crysl
+++ b/BouncyCastle/src/PaddedBufferedBlockCipher.crysl
@@ -39,6 +39,8 @@ CONSTRAINTS
 	plainTextOffset >= 0;
 	plainTextLen > 0;
 	cipherTextOffset >= 0;
+
+	padding in {ISO, Padding58,ESP}// BSI recoomedation for padding Scheme (ISO-Padding, Padding according to [58], ESP-Padding)
 	
 REQUIRES
 	generatedRijndaelEngine[cipher];
diff --git a/JavaCryptographicArchitecture/src/KeyPairGenerator.crysl b/JavaCryptographicArchitecture/src/KeyPairGenerator.crysl
index eba3b95..5c62b29 100644
--- a/JavaCryptographicArchitecture/src/KeyPairGenerator.crysl
+++ b/JavaCryptographicArchitecture/src/KeyPairGenerator.crysl
@@ -25,16 +25,19 @@ ORDER
 	Get, Init, Gen
 
 CONSTRAINTS
-	algorithm in {"RSA", "EC", "DSA", "DiffieHellman", "DH"}; //BSI TR-02102-1 Recommends atleast 3000bits for keys
-	algorithm in {"RSA"} => keysize in {4096, 3072};
-	algorithm in {"DSA"} => keysize in {3072};
-	algorithm in {"DiffieHellman", "DH"} => keysize in {3072};
-	algorithm in {"EC"} => keysize in {256};
+	algorithm in {"RSA", "EC", "DSA", "DiffieHellman", "DH"};
+	algorithm in {"RSA"} => keysize >=3000;
+	algorithm in {"DSA"} => keysize >= 3072;
+	algorithm in {"DiffieHellman", "DH"} => keysize >=3000;
+	algorithm in {"EC"} => keysize >=250;
+
+FORBIDDEN
+    algorithm =="DSA" && afterYear>=2029;
 
 REQUIRES
 	algorithm in {"RSA"} => preparedRSA[params];
 	algorithm in {"DSA"} => preparedDSA[params];
-	algorithm in {"DiffieHellman", "DH"} => preparedDH[params];
+	algorithm in {"DiffieHellman","DH"} => preparedDH[params];
 	algorithm in {"EC"} => preparedEC[params];
 
 ENSURES
diff --git a/JavaCryptographicArchitecture/src/RSAKeyGenParameterSpec.crysl b/JavaCryptographicArchitecture/src/RSAKeyGenParameterSpec.crysl
index ada8f2d..3e66bf8 100644
--- a/JavaCryptographicArchitecture/src/RSAKeyGenParameterSpec.crysl
+++ b/JavaCryptographicArchitecture/src/RSAKeyGenParameterSpec.crysl
@@ -12,7 +12,7 @@ ORDER
 	Con
 	
 CONSTRAINTS
-	keysize in {3072, 4096}; //BSI TR-02102-1 Recommends atleast 3000bits for keys
+	keysize >= 3000; //BSI TR-02102-1 Recommends atleast 3000bits for keys
 	publicExponent in {65537};
 	 
 ENSURES
diff --git a/Tink/src/AeadKeyTemplates.crysl b/Tink/src/AeadKeyTemplates.crysl
index 678ad13..e26b80d 100644
--- a/Tink/src/AeadKeyTemplates.crysl
+++ b/Tink/src/AeadKeyTemplates.crysl
@@ -28,7 +28,7 @@ OBJECTS
 	int key;
 	int iv; 
 	
-	com.google.crypto.tink.proto.HashType hashType;  // HashType enum: (1) - SHA1, (3) - SHA256, and (4) - SHA 512. 
+	com.google.crypto.tink.proto.HashType hashType;  // HashType enum: (1) - SHA2, (3) - SHA256, and (4) - SHA 512.
 	
 EVENTS
 	aes_gcm_evt : kt = createAesGcmKeyTemplate(key);
diff --git a/Tink/src/MacKeyTemplates.crysl b/Tink/src/MacKeyTemplates.crysl
index c931089..4da7841 100644
--- a/Tink/src/MacKeyTemplates.crysl
+++ b/Tink/src/MacKeyTemplates.crysl
@@ -22,7 +22,7 @@ OBJECTS
 	int key;
 	int tag; 
 	
-	int hashType;  // HashType enum: (1) - SHA1, (3) - SHA256, and (4) - SHA 512. 
+	int hashType;  // HashType enum: (1) - SHA2, (3) - SHA256, and (4) - SHA 512.
 	
 EVENTS
 	hmac_sha256_evt : hmac_sha256 = createHmacKeyTemplate(key, tag, _);