tographic Abstract Machine Dean Rosenzweig and Davor Runje University of Zagreb The Cryptographic Abstract Machine is an executional model of cryptographic actions, independent of the concrete cryptographic proemployed, even of the abstraction level of the underlying model of cryptography. This is motivated both by a theoretical purpose of relatdynamics of protocol executions at different levels of abstraction, and by a practical purpose of enabling automatic generation of provably correct code implementing protocol roles from high level specifications. Here we define the CrAM and show how slightly refurbished message patterns of [RRS03] can be compiled to CrAM code both for analysis and for creation of messages, and prove the correctness and completeness of that compilation.