In this paper we propose
as a formal model of computation in heterogenous networks of computers, humans and their devices, where these new procedures run; and we introduce
Procedure Derivation Logic
(PDL) as a framework for reasoning about security in actor-networks, as an extension of our previous
Protocol Derivation Logic
. Both formalisms are geared towards graphic reasoning. We illustrate its workings by analysing a popular form of two-factor authentication.