The overall goal of this project is to investigate complexity-based cryptography from two different angles. First we intend to apply formal methods to security complexity-based cryptographic definitions to give raise to practical and robust notions of security as well as corresponding verification techniques. In particular, we focus on defining anonymous communication against strong adversarial behavior (active attacks by standard computationally bounded adversaries), and cryptographic-based compilation of decentralized access control policies. Secondly, we intend to explore more efficient secure cryptographic primitives implementations. In particular, we intend to achieve fast, and side-channel-attack resistant implementations of traditional primitives, such as those related to asymmetric methods based on factorization and discrete logarithm, but also the more recent pairing-based primitives and those primitives arising from the study of the so-called post-quantum cryptographic schemes, based on coding and lattice theory. Such faster implementations often arise from deeper studies of the underlying theory thus requiring formal proof of their correctness and security.