Computational indistinguishability is one of the most central concepts in modern cryptography, and many other definitions (e.g. pseudorandomness, security of cryptographic schemes) can be formulated in terms of CI. We present the results of a study directed towards giving a direct and precise characterization of computational indistinguishability in an higher-order functional language for polynomial time computability, in which tools from implicit computational complexity and coinduction both play a central role. This is joint work with Alberto Cappai.