Modern cryptography is a realm of complex constructions with Probaibilistic
Polynomial-Time Turing (PPT) machines, viewed up to observational
equivalence
modulo negligible functions. Modern authentication protocols often involve
Bayesian reasoning about heterogenous channels. Formal security proofs
sometimes turn out to be as unreliable as the systems that they prove
secure. I
shall show how categorical and coalgebraic tools help with these problems.