ASECOLAB | Physical, social and cyber security

Actor networks

As computation spreads from computers to networks of computers, and migrates into cyberspace, it ceases to be globally programmable, but it remains programmable indirectly and partially: network computations cannot be controlled, but they can be steered by imposing local constraints on network nodes. Security tasks can be viewed as the tasks to “program” global behaviors through local constraints. Security protocols can be viewed as the “program particles” that assure that a system of local interactions leads towards some desired global goals. They are the patterns underlying software connectors of modern, world wide software systems.

As computation spreads beyond cyberspace, into physical and social spaces, new security tasks and problems arise. As computer networks increasingly merge with social networks, computer security and network security blend with much older security processes, underlying social, economic, and political life. We propose actor-networks as a mathematical formalism for incremental reasoning about security in heterogenous networks of computers, humans and their devices. This framework has been developed in joint work with Cathy Meadows. It supports graphic reasoning about networks, about processes and protocol interactions, and about each participant’s view and assurances. Here we show two types of diagrams, supporting these reasoning layers. Please see our recent papers (all joint work with Catherine Meadows) for more:

Formalizing physical security procedures
Actor-network procedures: Modeling multi-factor authentication, device pairing, social interactions (working paper; extended abstract in ICDCIT 2012)

This work is closely related to some of our earlier papers:

and all of it is based on Protocol Derivation Logic, which evolved through all of our past work, but is still waiting to be completely formalized and spelled out in a paper devoted just to that.