diff --git a/BouncyCastle/src/AsymmetricCipherKeyPair.crysl b/BouncyCastle/src/AsymmetricCipherKeyPair.crysl index 8eea7838..a0899fef 100644 --- a/BouncyCastle/src/AsymmetricCipherKeyPair.crysl +++ b/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; \ No newline at end of file + generatedECKeyPair[this] after Con; + generatedRSAKeyPair[this] after Con; + generatedECPubkey[pubKey] after getPub; + generatedECPrivkey[priKey] after getPri; + generatedRSAPubkey[pubKey] after getPub; + generatedRSAPrivkey[priKey] after getPri; + diff --git a/BouncyCastle/src/ECDHBasicAgreement.crysl b/BouncyCastle/src/ECDHBasicAgreement.crysl new file mode 100644 index 00000000..bb734ff1 --- /dev/null +++ b/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; diff --git a/BouncyCastle/src/HMac.crysl b/BouncyCastle/src/HMac.crysl index ae6be0af..cc1a24dc 100644 --- a/BouncyCastle/src/HMac.crysl +++ b/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]; - \ No newline at end of file diff --git a/BouncyCastle/src/IESCipher.crysl b/BouncyCastle/src/IESCipher.crysl new file mode 100644 index 00000000..8cbe5acc --- /dev/null +++ b/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]; + \ No newline at end of file diff --git a/BouncyCastle/src/IESEngine.crysl b/BouncyCastle/src/IESEngine.crysl new file mode 100644 index 00000000..44dbdc8a --- /dev/null +++ b/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; diff --git a/BouncyCastle/src/IESParameterSpec.crysl b/BouncyCastle/src/IESParameterSpec.crysl new file mode 100644 index 00000000..812df0f5 --- /dev/null +++ b/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]; diff --git a/BouncyCastle/src/IESWithCipherParameters.crysl b/BouncyCastle/src/IESWithCipherParameters.crysl new file mode 100644 index 00000000..f934b9a3 --- /dev/null +++ b/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; diff --git a/BouncyCastle/src/IESparameters.crysl b/BouncyCastle/src/IESparameters.crysl new file mode 100644 index 00000000..d80fec96 --- /dev/null +++ b/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; diff --git a/BouncyCastle/src/KDF2BytesGenerator.crysl b/BouncyCastle/src/KDF2BytesGenerator.crysl new file mode 100644 index 00000000..746354bc --- /dev/null +++ b/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]; diff --git a/BouncyCastle/src/KDFParameters.crysl b/BouncyCastle/src/KDFParameters.crysl new file mode 100644 index 00000000..c1ce3cde --- /dev/null +++ b/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]; diff --git a/BouncyCastle/src/KeyParameter.crysl b/BouncyCastle/src/KeyParameter.crysl index dd6496fa..3924d19e 100644 --- a/BouncyCastle/src/KeyParameter.crysl +++ b/BouncyCastle/src/KeyParameter.crysl @@ -17,4 +17,4 @@ REQUIRES randomized[key]; ENSURES - generatedKeyParameter[this]; \ No newline at end of file + generatedKeyParameter[this];