Merge pull request #158 from CROSSINGTUD/feature/required_predicates_…

…with_this Required predicates with this
CROSSINGTUD · Feb 5, 2024 · 8713ba8 · 8713ba8
2 parents fb3627e + 85f27e7
commit 8713ba8
Show file tree

Hide file tree

Showing 12 changed files with 29 additions and 8 deletions.
diff --git 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
@@ -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;
-
diff --git 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;
+	generatedPrivkey[retPrivateKey] after GetPriv;
diff --git 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
@@ -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
@@ -12,11 +12,12 @@ EVENTS
 
 ORDER
 	GetEnc*, Destroy?
+
+REQUIRES
+	generatedKey[this, _];
 
 ENSURES
 	preparedKeyMaterial[keyMaterial] after GetEnc;
 
 NEGATES
 	generatedKey[this, _] after Destroy;
-
-
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -12,6 +12,9 @@ EVENTS
 
 ORDER
 	GetEnc*, Destroy?
+
+REQUIRES
+	generatedKey[this, _];
 
 ENSURES
 	preparedKeyMaterial[keyMaterial] after GetEnc;