ASM View of Abstract Cryptography

The computational model of cryptography views agents as PPT algorithms operating on strings. In the abstract model, agents are working on syntactic representations of messages, using a fixed set of rules for composing and analyzing such representations. By the Abstract State Machine thesis of Gurevich, an agent in the abstract model is an algorithm, simulatable by an appropriate ASM. But what are the appropriate algorithms for such agents? What are their states? What kind of algorithms are they: simple (isolated, sequential, small-step), interactive (between and within a step), parallel (wide-step, with interacting components), distributed? It turns out that a surprisingly simple model is faithful with respect to the computational model. The basic PPT computational notions, of indistinguishability and unforgeability, are given sharp abstract counterparts, allowing porting of typical proofs between the two abstraction levels, both ways. As a proof of the practical value of the model, a tool demo of a general-purpose software-testing tool developed in MSR, SpecExplorer, finding attacks on abstract cryptographic protocols will be presented.