Skip to content

CONSTRAINTS and REQUIRES sections are different from the expected for Cipher.spec #66

@fillypenascimento

Description

@fillypenascimento

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];

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions