Poster: The Beauty and the Beast (40 years of process algebra and cybersecurity) 1st Silvia De Francisci SySMA Unit IMT School for Advanced Studies Lucca, Italy silvia.defrancisci@imtlucca.it 2nd Gabriele Costa SySMA Unit IMT School for Advanced Studies Lucca, Italy gabriele.costa@imtlucca.it 3rd Rocco De Nicola SySMA Unit IMT School for Advanced Studies Lucca, Italy rocco.denicola@imtlucca.it Abstract—Process algebras provide the mathematical foun- dation for several formal verification techniques, and they profoundly influenced many fields, from correct design to testing. Process algebras were greatly influential also for the security community. One of the main reasons for their success is their compact, yet expressive and flexible syntax, which allows to model the relevant aspects of computation while abstracting away the secondary ones. Although most authors acknowledge the importance of process algebras for the security community, it is not trivial to estimate how they shaped the past and present researches. The goal of this work is to provide a comprehensive outlook on some prominent works about process algebras and security. These include both the application of process algebras to security problems and process algebras inspired by security-related aspects of computation. To achieve this, we consider three fundamental fields of cybersecurity, i.e., secure development, threat modeling and vulnerability assess- ment. Index Terms—process algebra, cybersecurity, formal meth- ods in security. 1. Introduction Process Algebras (PA) are formal languages com- monly used to model the behavior of a computational agent. Roughly speaking, PA put most of the emphasis on the control flow structure of the modeled agent, rather than on its data flow. In most PA, computational steps also emit observable actions. This allows to elegantly introduce the role of an external observer, i.e., someone who aims at understanding an agent’s behavior, but has no control on its internal structure. Under reasonable assumptions, an attacker is, in fact, an external observer. As a matter of fact, an attacker is generally represented by its capa- bilities and goals. In terms of capabilities, the possibility to partially interact with the agent’s I/O mechanism is a typical setting (e.g., think of information flow [19]). In terms of goals, the attacker’s aim can be modeled as a target state, e.g., denoting a failure of the agent, she wants to reach. Formal models of both the attacker and the system are the fundamental building blocks of most automated, formal reasoning techniques. Not surprisingly, a vast literature about the adoption of PA in cybersecurity exists. As a result, determining the overall influence of PA in cybersecurity and its sub-fields is difficult. This poster proposes a systematization of the existing PA and their applications to the cybersecurity fields. Our contributions are the following.1 • We show significant PA from a genealogy stand- point, as well as their unique characteristics. • We discuss the impact of some PA and its ge- nealogy in three application scenarios for cyberse- curity classification: Secure Development, Threat modeling, and Vulnerability assessment. • We show the state-of-the-art of PA for secure Development Life Cycle (DLC). 2. Genealogy of PA The genesis of PA goes back to the 80s, when a few authors independently proposed different calculi for the specification of processes: Milner’s Calculus of Communicating Systems (CCS) [16], Brookes, Hoare and Roscoe’s Communicating Seqential Processes (CSP) [8], and Bergstra’s Algebra of Communicating Processes (ACP) [6], which inspired a considerable number of other PA. Typically, derived PA introduce some new elements w.r.t. their archetypes. These elements often aim to model some specific aspects of computation. In order to better highlight these extensions we label PA with icons de- noting their peculiar features. Such features include the ability to model security asp