Constructive Cryptography in HOL: the Communication Modeling Aspect by Andreas Lochbihler and S. Reza Sefidgar Mar 17