We introduce an executable formal model of abstract encryption using the specification language AsmL, based on Abstract State
Machines of Gurevich, providing a simple executable models for cryptographic protocols. We show strong universality properties
of our descriptions of patterns, protocol roles and environment behaviors-no ASM program can do better, given the same information.