2011/06/03 by Duško Pavlović, Dusko Pavlovic, Pavlovic, Dusko +2
Computer Science · Social Sciences · #Access Control and Trust #Advanced Authentication Protocols Security #Computers and Society (cs.CY) #Cryptography and Security (cs.CR) #D.4.4 #D.4.6 #FOS: Computer and information sciences #K.4.2 #K.6.5 #Logic in Computer Science (cs.LO) #Social and Information Networks (cs.SI) #User Authentication and Security Systems #cs.CR #cs.CY #cs.LO #cs.SI
paper · pdf · doi:10.48550/arxiv.1106.0706
32 pages, 12 figures, 3 tables; journal submission; extended references, added discussion
openalex publication_date 2011/06/03 · arxiv created 2011/08/29 · arxiv updated 2011/08/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
As computation spreads from computers to networks of computers, and migrates into cyberspace, it ceases to be globally programmable, but it remains programmable indirectly: network computations cannot be controlled, but they can be steered by local constraints on network nodes. The tasks of "programming" global behaviors through local constraints belong to the area of security. The "program particles" that assure that a system of local interactions leads towards some desired global goals are called security protocols. As computation spreads beyond cyberspace, into physical and social spaces, new security tasks and problems arise. As networks are extended by physical sensors and controllers, including the humans, and interlaced with social networks, the engineering concepts and techniques of computer security blend with the social processes of security. These new connectors for computational and social software require a new "discipline of programming" of global behaviors through local constraints. Since the new discipline seems to be emerging from a combination of established models of security protocols with older methods of procedural programming, we use the name procedures for these new connectors, that generalize protocols. In the present paper we propose actor-networks as a formal model of computation in heterogenous networks of computers, humans and their devices; and we introduce Procedure Derivation Logic (PDL) as a framework for reasoning about security in actor-networks. On the way, we survey the guiding ideas of Protocol Derivation Logic (also PDL) that evolved through our work in security in last 10 years. Both formalisms are geared towards graphic reasoning and tool support. We illustrate their workings by analysing a popular form of two-factor authentication, and a multi-channel device pairing procedure, devised for this occasion.