Is a ruler-and-compass algorithm executable by a Turing machine? Yes, but at a level of abstraction far remote from the intended one. These are, for all purposes, two different algorithms, though linked by a notion of simulation (supported by sediments of mathematics). The `behavioral theory of algorithms', developed in this century by Y.Gurevich (and others, foremostly A. Blass) insists on the distinction.

If so, what is an algorithm? By intended abstraction, algorithms come in several species: simple (isolated, sequential, small-step), interactive (between steps, and, since one algorithm's complex protocol is another algorithm's step, also within a step), parallel (wide-step, with interacting components), distributed ... The purpose of this talk is to present the basic ideas and results of the theory under development, emphasizing several new twists in which the author is involved.

In particular, what is abstract cryptography about, how do we abstract from the interactive algorithms of computational cryptography? It turns out that the basic PPT computational notions, of indistinguishability and unforgeability, have sharp abstract counterparts, allowing porting of typical proofs between the two abstraction levels, both ways. How can this be useful, except for proofs-by-hand? Several species of algorithms are provably encodable in AsmL/Spec# (by intention they should all be, extending the programming languages if not otherwise), and, time permitting, a tool demo, of a general-purpose software-testing tool developed in MSR, SpecExplorer, finding attacks on abstract cryptographic protocols, given a straightforward protocol model, will be presented.