Cache-based attacks are potent threats to modern multi-core computing systems. Countermeasures against such attacks try to randomize the address-to-set mapping of the caches so that the adversary cannot easily extract the mapping profile of the cache — an essential prerequisite for the attacks. However, all the existing proposals are based on empirical security analyses, and many have severe security pitfalls discovered later. In this project, we aim to address the randomized cache design problem cryptographically, providing a formal foundation for the problem with concrete definitions for the adversary and the primitives and eventually providing reduction-based proofs of security. Based on a preliminary observation that address-to-set mapping can be viewed as a special type of hashing, and the cache attacks can be modelled as multicollisions on such hashes, we envision an approach for constructing such security proofs. Broadly, this work would initiate the formal cryptographic treatment of various micro-architectural attacks and their countermeasures, which is desirable for any security paradigm but is missing so far in the realm of microarchitectural attacks.