On branch add-tests, the generated spec for Android-cc, 0108 version Cipher.spec is not as expected.
-> Section CONSTRAINTS presented unfinished constraints like this:
part(0,transformation) in {"AES"} => part(1,transformation) in ${aes_modes};
and this
part(0,transformation) in {"RSA"} => part(2,transformation) in ${rsa_paddings};
where the expected results should look like
part(0,"/",transformation) in {"AES"} => part(1,"/",transformation) in {"OFB", "CBC", "CTS", "CTR", "CFB"};
and
part(0,"/",transformation) in {"RSA"} => part(2,"/",transformation) in {"NoPadding", "PKCS1Padding", ""};.
-> Section REQUIRES presented require expressions with null's
generatedKey[key,null]; and preparedAlg[param,null];
where the expected results should be
generatedKey[key, part(0,"/",transformation)]; and preparedAlg[param, part(0,"/",transformation)];
Here is the plain spec for the cited sections:
// Cipher.spec for Android-cc version 0108
CONSTRAINTS
part(1,transformation) in {"CBC","PCBC","CTR","CTS","CFB","OFB"} && encmode!=1 => noCallTo[IWOIV];
part(1,transformation) in {"CBC","PCBC","CTR","CTS","CFB","OFB"} && encmode==1 => callTo[iv];
encmode in {1,2,3,4};
length[pre_plaintext]>=pre_plain_off+len;
length[pre_ciphertext]<=pre_ciphertext_off;
length[plainText]<=plain_off+len;
length[cipherText]<=ciphertext_off;
part(0,transformation) in {"AES"} => part(1,transformation) in ${aes_modes};
part(0,transformation) in {"AES"} && part(1,transformation) in {"CBC"} => part(2,transformation) in {"PKCS7Padding","PKCS5Padding","ISO10126Padding"};
part(0,transformation) in {"AES"} && part(1,transformation) in {"CTR","CFB","OFB"} => part(2,transformation) in {"NoPadding"};
part(0,transformation) in {"RSA"} => part(1,transformation) in {"","ECB"};
part(0,transformation) in {"RSA"} => part(2,transformation) in ${rsa_paddings};
part(0,transformation) in {"AES","RSA"};
REQUIRES
generatedKey[key,null];
randomized[ranGen];
preparedAlg[param,null];
!macced[_,plainText];
part(1,transformation) in {"CBC","PCBC","CTR","CTS","CFB","OFB"} && encmode==1 => preparedIV[params];
part(1,transformation) in {"GCM"} => preparedGCM[params];
On branch add-tests, the generated spec for Android-cc, 0108 version Cipher.spec is not as expected.
-> Section CONSTRAINTS presented unfinished constraints like this:
part(0,transformation) in {"AES"} => part(1,transformation) in ${aes_modes};and this
part(0,transformation) in {"RSA"} => part(2,transformation) in ${rsa_paddings};where the expected results should look like
part(0,"/",transformation) in {"AES"} => part(1,"/",transformation) in {"OFB", "CBC", "CTS", "CTR", "CFB"};and
part(0,"/",transformation) in {"RSA"} => part(2,"/",transformation) in {"NoPadding", "PKCS1Padding", ""};.-> Section REQUIRES presented require expressions with null's
generatedKey[key,null];andpreparedAlg[param,null];where the expected results should be
generatedKey[key, part(0,"/",transformation)];andpreparedAlg[param, part(0,"/",transformation)];Here is the plain spec for the cited sections: