WIP Adding necessary crysl rules to support ECIES

BouncyCastle/src/AsymmetricCipherKeyPair.crysl

@@ -3,16 +3,33 @@ SPEC org.bouncycastle.crypto.AsymmetricCipherKeyPair
 OBJECTS
 	org.bouncycastle.crypto.params.AsymmetricKeyParameter pubParams;
 	org.bouncycastle.crypto.params.AsymmetricKeyParameter privParams;
+	java.security.PrivateKey priKey;
+	java.security.PublicKey pubKey;
 
 EVENTS
-	co : AsymmetricCipherKeyPair(pubParams, privParams);
+	Con: AsymmetricCipherKeyPair(pubParams, privParams);
 
+	getPri : priKey = getPrivate();
+
+	getPub : pubKey = getPublic();
+
 ORDER
-	co
+	Con, (getPri*, getPub*)*
+
+CONSTRAINTS
+	instanceOf[pubParams, org.bouncycastle.crypto.params.ECPublicKeyParameters] => instanceOf[privParams, org.bouncycastle.crypto.params.ECPrivateKeyParameters];
+	instanceOf[pubParams, org.bouncycastle.crypto.params.RSAKeyParameters] => instanceOf[privParams, org.bouncycastle.crypto.params.RSAPrivateCrtKeyParameters];
 
-REQUIRES
-	generatedRSAKeyParameters[pubParams];
-	generatedRSAPrivateCrtKeyParameters[privParams];
+REQUIRES	
+	generatedRSAKeyParameters[pubParams] || generatedECPublicKeyParameters[pubParams];
+	generatedRSAPrivateCrtKeyParameters[privParams] || generatedECPrivateKeyParameters[privParams];
+
 
 ENSURES
-	generatedRSAKeyPair[this] after co;
+	generatedECKeyPair[this] after Con;
+	generatedRSAKeyPair[this] after Con;
+	generatedECPubkey[pubKey] after getPub;
+	generatedECPrivkey[priKey] after getPri;
+	generatedRSAPubkey[pubKey] after getPub;
+	generatedRSAPrivkey[priKey] after getPri;
+

BouncyCastle/src/ECDHBasicAgreement.crysl

@@ -0,0 +1,19 @@
+SPEC org.bouncycastle.crypto.agreement.ECDHBasicAgreement
+
+OBJECTS
+	int fieldSize;
+	org.bouncycastle.crypto.CipherParameters privParam;
+	org.bouncycastle.crypto.CipherParameters pubParam;
+
+EVENTS
+	Calc : calculateAgreement(pubParam);
+
+	Init : init(privParam);
+
+	Con : ECDHBasicAgreement();
+
+ORDER
+	Con, (Init, Calc)+
+
+ENSURES
+	generatedECDHBasicAgreement[this] after Con;

BouncyCastle/src/HMac.crysl

@@ -6,30 +6,27 @@ OBJECTS
 	byte[] output;
 
 EVENTS
-	c1 : HMac(digest);
-	c2 : HMac(digest, _);
-	Cons := c1 | c2;
+	con1 : HMac(digest);
+	con2 : HMac(digest,_);
+	Cons := con1 | con2;
 
 	Init : init(params);
 
-	u1 : update(_);
-	u2 : update(_, _, _);
 
-	Updates := u1 | u2;
+	upd1 : update(_);
+	upd2 : update(_,_,_);
+	Updates := upd1 | upd2;
 
-	f1 : doFinal(output, _);
+	Final : doFinal(output,_);
 
-	Finals := f1;
-
-	r : reset();
 
 ORDER
-	Cons, (Init, Updates+, Finals)+
+	Cons, (Init, Updates+, Final)+
 
 REQUIRES
 	generatedSHA256Digest[digest];
 	generatedKeyParameter[params];
 
 ENSURES
+	generatedHMac[this] after Cons;
 	macced[output];
-

BouncyCastle/src/IESCipher.crysl

@@ -0,0 +1,54 @@
+SPEC org.bouncycastle.jcajce.provider.asymmetric.ec.IESCipher
+OBJECTS
+	byte[] plaintext;
+	byte[] ciphertext;
+
+	java.security.Key key;
+	java.security.SecureRandom ranGen;
+	java.security.spec.AlgorithmParameterSpec paramSpec;
+
+	int iv_len;
+	int encmode;
+	int plain_len;
+	int plain_off;
+	int ciphertext_off;
+
+	java.security.AlgorithmParameters params;
+	org.bouncycastle.crypto.engines.IESEngine engine;
+
+EVENTS
+	con1 : IESCipher(engine);
+	con2 : IESCipher(engine, iv_len);
+	Cons := con1 | con2;
+
+	init1 : engineInit(encmode, key, params, ranGen);
+	init2 : engineInit(encmode, key, ranGen); //guesses paramSpec//*
+	init3 : engineInit(encmode, key, paramSpec, ranGen);
+	Inits := init1 | init2 | init3;
+
+	upd1 : engineUpdate(plaintext, plain_off, plain_len);
+	upd2 : engineUpdate(plaintext, plain_off, plain_len, ciphertext, ciphertext_off);
+	Updates := upd1 | upd2;
+
+	doFinal1 : ciphertext = engineDoFinal(plaintext, plain_off, plain_len);
+	doFinal2 : engineDoFinal(plaintext, plain_off, plain_len, ciphertext, ciphertext_off);
+	DoFinals := doFinal1 | doFinal2;
+
+ORDER
+	Cons, (Inits, Updates*, DoFinals)+
+
+CONSTRAINTS
+	encmode in {1,2,3,4};
+	length[plaintext] <= plain_off + plain_len;
+	length[ciphertext] <= ciphertext_off;
+
+REQUIRES
+	generatedIESEngine[engine];
+	generatedIESParameterSpec[paramSpec] || generatedIESParameter[params];
+	randomized[ranGen];
+	generatedPubkey[key] || generatedPrivkey[key] || generatedECPubkey[key] || generatedECPrivkey[key];
+
+ENSURES
+	generatedIESCipher[this] after Inits;
+	encrypted[ciphertext, plaintext];
+

BouncyCastle/src/IESEngine.crysl

@@ -0,0 +1,55 @@
+SPEC org.bouncycastle.crypto.engines.IESEngine
+
+OBJECTS
+	byte[] plain;
+	byte[] ciphertext;
+	int plain_off;
+	int plain_len;
+
+	boolean encmode;
+
+	org.bouncycastle.crypto.DerivationFunction derivFun;
+	org.bouncycastle.crypto.BasicAgreement agr;
+	org.bouncycastle.crypto.BufferedBlockCipher bufBloCip;
+	org.bouncycastle.crypto.Mac mac;
+
+	org.bouncycastle.crypto.CipherParameters priParams;
+	org.bouncycastle.crypto.CipherParameters pubParams;
+	org.bouncycastle.crypto.CipherParameters params;
+
+	org.bouncycastle.crypto.KeyParser keyParser;
+	org.bouncycastle.crypto.generators.EphemeralKeyPairGenerator ephKeyPairGen;
+	org.bouncycastle.crypto.params.AsymmetricKeyParameter ecKey;
+
+
+EVENTS
+	con1 : IESEngine(agr, derivFun, mac);
+	con2 : IESEngine(agr, derivFun, mac, bufBloCip);
+	Cons := con1 | con2;
+
+	init1: init(encmode, priParams, pubParams, params);
+	init2: init(ecKey, params, ephKeyPairGen); //decryptor//*
+	init3: init(ecKey, params, keyParser); //encryptor//*
+	Inits:= init1 | init2 | init3;
+
+	Proc : ciphertext = processBlock(plain, plain_off, plain_len);
+
+ORDER
+	Cons, (Inits, Proc)+
+
+CONSTRAINTS
+	length[plain] <= plain_off + plain_len;
+
+REQUIRES
+	generatedBufferedBlockCipher[bufBloCip];
+	generatedIESParameters[params] || IESWithCipherParameters[params];
+	generatedCipherParams[priParams]; 
+	generatedCipherParams[pubParams];
+	generatedKDF2BytesGenerator[derivFun];
+	generatedECDHBasicAgreement[agr];
+	generatedHMAC[mac];
+	generatedECPubkey[ecKey] || generatedECPrivkey[ecKey];
+
+ENSURES
+	generatedIESEngine[this] after Cons;
+	encrypted[ciphertext] after Proc;

BouncyCastle/src/IESParameterSpec.crysl

@@ -0,0 +1,30 @@
+SPEC org.bouncycastle.jce.spec.IESParameterSpec
+
+OBJECTS
+	int cipherKeySize;
+	int macKeySize;
+	byte[] nonce;
+	byte[] derivation;
+	byte[] encoding;
+	boolean compress;
+
+EVENTS
+	d : getDerivationV();
+
+	e : getEncodingV();
+
+	con1 : IESParameterSpec(derivation, encoding, macKeySize, cipherKeySize, nonce, compress);
+	con2 : IESParameterSpec(derivation, encoding, macKeySize, cipherKeySize, nonce);
+	con3 : IESParameterSpec(derivation, encoding, macKeySize);
+	Cons := con1 | con2 | con3;
+
+ORDER
+	Cons, (d | e)*
+
+CONSTRAINTS
+	macKeySize >= 128;
+	cipherKeySize >= 128;
+	noCallTo[con3];
+
+ENSURES
+	generatedIESParameterSpec[this];

BouncyCastle/src/IESWithCipherParameters.crysl

@@ -0,0 +1,22 @@
+SPEC org.bouncycastle.crypto.params.IESWithCipherParameters
+OBJECTS
+	int keySize;
+	byte[] derivation;
+	byte[] encoding;
+	int macKeySize;
+	int cipherKeySize;
+
+EVENTS
+	Con : IESWithCipherParameters(derivation, encoding, macKeySize, cipherKeySize );
+
+	Get : keySize = getCipherKeySize();
+
+ORDER
+	Con, Get*
+
+CONSTRAINTS
+	macKeySize >= 128;
+	cipherKeySize >= 128;
+
+ENSURES
+	generatedIESWithCipherParameters[this] after Con;

BouncyCastle/src/IESparameters.crysl

@@ -0,0 +1,23 @@
+SPEC org.bouncycastle.crypto.params.IESParameters
+OBJECTS
+	int macKeySize;
+	byte[] derivation;
+	byte[] encoding;
+
+EVENTS
+	getMac : getMacKeySize();
+
+	getDer : getDerivationV();
+
+	getEnc : getEncodingV();
+
+	Con : IESParameters(derivation, encoding, macKeySize);
+
+ORDER
+	Con, (getMac | getDer | getEnc)*
+
+CONSTRAINTS
+	macKeySize >= 128;
+
+ENSURES
+	generatedIESParameters[this] after Con;

BouncyCastle/src/KDF2BytesGenerator.crysl

@@ -0,0 +1,25 @@
+SPEC org.bouncycastle.crypto.generators.KDF2BytesGenerator
+
+OBJECTS
+	byte[] out;
+	org.bouncycastle.crypto.DerivationParameters params;
+	org.bouncycastle.crypto.Digest digest;
+	int outLen;
+	int outOff;
+
+EVENTS
+	Con: KDF2BytesGenerator(digest);
+
+	Init : init(params);
+
+	Gen : generateBytes(out, outOff, outLen);
+
+ORDER
+	Con, (Init, Gen)+
+
+REQUIRES
+	generatedSHA256Digest[digest];
+	generatedKDFParameters[params];
+
+ENSURES
+	generatedKDF2BytesGenerator[this];

BouncyCastle/src/KDFParameters.crysl

@@ -0,0 +1,14 @@
+SPEC org.bouncycastle.crypto.params.KDFParameters
+
+OBJECTS
+	byte[] iv;
+	byte[] shared;
+
+EVENTS
+	Con: KDFParameters(shared, iv);
+
+ORDER
+	Con
+
+ENSURES
+	generatedKDFParameters[this];

BouncyCastle/src/KeyParameter.crysl

@@ -17,4 +17,4 @@ REQUIRES
 	randomized[key];
 
 ENSURES
-	generatedKeyParameter[this];
+	generatedKeyParameter[this];