Program synthesis of cryptographic algorithms requires automatically checking the security properties of the generated program. We focus on Linicrypt algorithms, which may only use linear operations and a block cipher, allowing the use of linear algebra to analyze the security. We give a characterization of CPA-secure Linicrypt encryption schemes in terms of linear algebra. Using this characterization, we develop a sound and complete system to determine (in polynomial time) the CPA-security of Linicrypt block cipher modes with a single chaining value. Existing work fails to be complete, missing some block cipher modes that are secure.
As an application of our method, we classify all possible Linicrypt CPA-secure block cipher modes of operation that are optimal, i.e. make only a single oracle call for each message block.