Leak-proof protocol: is such a thing possible? Is it possible to design a protocol that by itself guarantees that a malicious implementation cannot leak secret data without breaking the protocol?

Setting:


Alice and Bob have a pre-shared secret key K. Using this key, Alice encrypts a bunch of plaintexts and sends them to Bob as a collection of files. The plaintexts are short-ish texts in a natural language.
Each plaintext is encrypted independently of others, and must be decryptable independently. Some sort of authenticated encryption is used. 
Eve receives a copy of the collection. This is the only data she gets (i.e. no timing or other side channels). She does not communicate with Alice (but can have a previous arrangement with her, e.g. pre-share some secret keys). Alice cannot communicate with Eve directly, or otherwise send out any data except as defined by this protocol.
We want to ensure that Alice cannot manipulate the encryption, without consequences detectable by Bob, in such a way that Eve can obtain information about the secret key. We assume that transmission is 100% reliable, so if Bob can't decrypt some of the files, he will conclude that Alice is a bad actor.
Also, obviously, we don't want Eve to obtain the plaintexts. It's tolerable if Eve can detect multiple copies of the same plaintext.




It seems that any kind of randomness in the protocol has to be excluded.

For example, if we use an encryption scheme with random IV which is prepended to the ciphertext, Alice can just encrypt the secret key K using another secret key known to Eve, Ke, and apply it instead of IV (IV := E(Ke, K)). Instant leak!

If our protocol adds randomness to the plaintext itself (before encryption), Alice still can manipulate the encryption result by choosing the random value. In the worst case she will have to use brute force, changing the random bits until specific bits of the ciphertext assume the values she wants. On average, she will need about 2n iterations to leak n bits of data. If, say, 1000 encryptions is a small enough number to be unnoticeable on any modern equipment (even "weak" such as a smartphone), then Alice would be able to leak ~10 bits of data per encrypted file.

The next thought I tried is to use deterministic encryption with Synthetic IV based on plaintext (similar to SIV-CTR construct). Besides obvious drawbacks caused by the low entropy of the natural-language plaintexts, this scheme still does not preclude Alice from leaking if she can manipulate plaintexts in a way not obvious to Bob. For example, she can try adding spaces at the ends of text lines, or insert some non-spacing Unicode chars, until she gets desired bit pattern in the ciphertext. (I don't know how to estimate the effort she'll need to leak n bits per ciphertext. Is it still O(2n), as in previous case?)

The last option seems better than others, because the manipulations are detectable by Bob, at least potentially. But this detection happens outside the domain of the protocol, and is not reliable. Are there other possibilities?
It doesn't work without further restrictions.

For simplification, let's assume Alice encrypts a bunch of files but doesn't have to send all of them to Bob. She can still decide to re-order the files or leave out some.

Then she can encode the secret shared key between Alice and Bob in the least significant bits of the ciphertexts without changing the files. She is only rearranging them so that Eve can extract the key. But if Bob checks the integrity of each message, it holds.

If more files are transmitted than the keylength, this works. Otherwise, more than one bit has to be encoded in less messages. And in order to get enough decryptable ciphertexts more files might have to be encrypted.