diff --git a/BouncyCastle-JCA/pom.xml b/BouncyCastle-JCA/pom.xml
index 0ba4362..3a8fbea 100644
--- a/BouncyCastle-JCA/pom.xml
+++ b/BouncyCastle-JCA/pom.xml
@@ -6,7 +6,6 @@
 	<artifactId>BouncyCastle-JCA</artifactId>
 	<version>3.0.2</version>
 	<name>CrySL Rules Bundle</name>
-
 	<licenses>
 		<license>
 			<name>Eclipse Public License - v2.0</name>
diff --git a/BouncyCastle-JCA/src/Key.crysl b/BouncyCastle-JCA/src/Key.crysl
index 948c3f6..510ddf9 100644
--- a/BouncyCastle-JCA/src/Key.crysl
+++ b/BouncyCastle-JCA/src/Key.crysl
@@ -2,14 +2,16 @@ SPEC java.security.Key
 
 OBJECTS 
 	byte[] keyMaterial;
-	
+
 EVENTS
 	ge1: keyMaterial = getEncoded();
 	GetEnc := ge1;
-	
+
 ORDER
 	GetEnc*
+
+REQUIRES
+	generatedKey[this, _] || generatedPubkey[this] || generatedPrivkey[this];
 	
 ENSURES
 	preparedKeyMaterial[keyMaterial] after GetEnc;
-	
\ No newline at end of file
diff --git a/BouncyCastle-JCA/src/KeyPair.crysl b/BouncyCastle-JCA/src/KeyPair.crysl
index 0baff04..b98f2ab 100644
--- a/BouncyCastle-JCA/src/KeyPair.crysl
+++ b/BouncyCastle-JCA/src/KeyPair.crysl
@@ -22,8 +22,9 @@ ORDER
 REQUIRES
 	generatedPrivkey[privateKey];
 	generatedPubkey[publicKey];
+	noCallTo[Con] => generatedKeypair[this, _];
 	
 ENSURES
 	generatedKeypair[this, _] after Con;
 	generatedPubkey[retPublicKey] after GetPubl;
-	generatedPrivkey[retPrivateKey] after GetPriv;
\ No newline at end of file
+	generatedPrivkey[retPrivateKey] after GetPriv;
diff --git a/BouncyCastle-JCA/src/PrivateKey.crysl b/BouncyCastle-JCA/src/PrivateKey.crysl
index ec3008c..265d05b 100644
--- a/BouncyCastle-JCA/src/PrivateKey.crysl
+++ b/BouncyCastle-JCA/src/PrivateKey.crysl
@@ -9,6 +9,9 @@ EVENTS
 
 ORDER
 	GetEnc*
+
+REQUIRES
+	generatedPrivkey[this];
 	
 ENSURES
 	preparedKeyMaterial[keyMaterial] after GetEnc;
diff --git a/BouncyCastle-JCA/src/PublicKey.crysl b/BouncyCastle-JCA/src/PublicKey.crysl
index e273315..941f828 100644
--- a/BouncyCastle-JCA/src/PublicKey.crysl
+++ b/BouncyCastle-JCA/src/PublicKey.crysl
@@ -9,6 +9,9 @@ EVENTS
 
 ORDER
 	GetEnc*
+
+REQUIRES
+	generatedPubkey[this];
 	
 ENSURES
 	preparedKeyMaterial[keyMaterial] after GetEnc;
diff --git a/BouncyCastle-JCA/src/SecretKey.crysl b/BouncyCastle-JCA/src/SecretKey.crysl
index 5433c58..8cc0cdf 100644
--- a/BouncyCastle-JCA/src/SecretKey.crysl
+++ b/BouncyCastle-JCA/src/SecretKey.crysl
@@ -12,11 +12,12 @@ EVENTS
 
 ORDER
 	GetEnc*, Destroy?
+
+REQUIRES
+	generatedKey[this, _];
 			
 ENSURES
 	preparedKeyMaterial[keyMaterial] after GetEnc;
 
 NEGATES
 	generatedKey[this, _] after Destroy;
-
-	
\ No newline at end of file
diff --git a/JavaCryptographicArchitecture/pom.xml b/JavaCryptographicArchitecture/pom.xml
index 2aac4b3..57a63f0 100644
--- a/JavaCryptographicArchitecture/pom.xml
+++ b/JavaCryptographicArchitecture/pom.xml
@@ -6,7 +6,6 @@
 	<artifactId>JavaCryptographicArchitecture</artifactId>
 	<version>3.0.2</version>
 	<name>CrySL Rules Bundle</name>
-
 	<licenses>
 		<license>
 			<name>Eclipse Public License - v2.0</name>
diff --git a/JavaCryptographicArchitecture/src/Key.crysl b/JavaCryptographicArchitecture/src/Key.crysl
index 44f9841..510ddf9 100644
--- a/JavaCryptographicArchitecture/src/Key.crysl
+++ b/JavaCryptographicArchitecture/src/Key.crysl
@@ -9,6 +9,9 @@ EVENTS
 
 ORDER
 	GetEnc*
+
+REQUIRES
+	generatedKey[this, _] || generatedPubkey[this] || generatedPrivkey[this];
 	
 ENSURES
 	preparedKeyMaterial[keyMaterial] after GetEnc;
diff --git a/JavaCryptographicArchitecture/src/KeyPair.crysl b/JavaCryptographicArchitecture/src/KeyPair.crysl
index 2a69a65..b98f2ab 100644
--- a/JavaCryptographicArchitecture/src/KeyPair.crysl
+++ b/JavaCryptographicArchitecture/src/KeyPair.crysl
@@ -22,6 +22,7 @@ ORDER
 REQUIRES
 	generatedPrivkey[privateKey];
 	generatedPubkey[publicKey];
+	noCallTo[Con] => generatedKeypair[this, _];
 	
 ENSURES
 	generatedKeypair[this, _] after Con;
diff --git a/JavaCryptographicArchitecture/src/PrivateKey.crysl b/JavaCryptographicArchitecture/src/PrivateKey.crysl
index ec3008c..265d05b 100644
--- a/JavaCryptographicArchitecture/src/PrivateKey.crysl
+++ b/JavaCryptographicArchitecture/src/PrivateKey.crysl
@@ -9,6 +9,9 @@ EVENTS
 
 ORDER
 	GetEnc*
+
+REQUIRES
+	generatedPrivkey[this];
 	
 ENSURES
 	preparedKeyMaterial[keyMaterial] after GetEnc;
diff --git a/JavaCryptographicArchitecture/src/PublicKey.crysl b/JavaCryptographicArchitecture/src/PublicKey.crysl
index e273315..941f828 100644
--- a/JavaCryptographicArchitecture/src/PublicKey.crysl
+++ b/JavaCryptographicArchitecture/src/PublicKey.crysl
@@ -9,6 +9,9 @@ EVENTS
 
 ORDER
 	GetEnc*
+
+REQUIRES
+	generatedPubkey[this];
 	
 ENSURES
 	preparedKeyMaterial[keyMaterial] after GetEnc;
diff --git a/JavaCryptographicArchitecture/src/SecretKey.crysl b/JavaCryptographicArchitecture/src/SecretKey.crysl
index 955e3c5..8cc0cdf 100644
--- a/JavaCryptographicArchitecture/src/SecretKey.crysl
+++ b/JavaCryptographicArchitecture/src/SecretKey.crysl
@@ -12,6 +12,9 @@ EVENTS
 
 ORDER
 	GetEnc*, Destroy?
+
+REQUIRES
+	generatedKey[this, _];
 			
 ENSURES
 	preparedKeyMaterial[keyMaterial] after GetEnc;