@inproceedings{VNC 2020, author = {Dantas, Yuri Gil and Nigam, Vivek and Talcott, Carolyn}, title = {A Formal Security Assessment Framework for Cooperative Adaptive Cruise Control}, booktitle = {IEEE Vehicular Networking Conference (VNC)}, publisher = {IEEE}, pages = {1-8}, year = {2020}, month = dec, abstract = {For increased safety and fuel-efficiency, vehicle platoons use Cooperative Adaptive Cruise Control (CACC) where vehicles adapt their state, incl. speed and position, based on information exchanged between vehicles. Intruders, however, may carry out attacks against CACC platoons by exploiting the communication channels used to cause harm, e.g., a vehicle crash. Therefore, during design-phase, engineers should provide evidence supporting platoon security. This paper proposes a formal framework for the security verification of CACC platoons to provide such evidence based on precise mathematical models. Our vehicle platoon models support the specification of both cyber, e.g., communication protocols, and physical, e.g., speeds, position, vehicle behaviors. Moreover, we propose intruder models that are parametric on his capabilities of manipulating communication channels, i.e., message injection and blocking. Our model is implemented enabling the automated formal verification involving both platoon and intruder models. We validate our machinery with a number of attacks taken from the literature and novel attacks discovered by using our formal machinery.}, doi = {10.1109/VNC51378.2020.9318334}, keywords = {attacks, formal verification, platoon, security, AutoFOCUS3, AF3}, } @inproceedings{alturki19cathy, author = {Alturki, Musab A. and Ban Kirigin, Tajana and Kanovich, Max and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn}, title = {A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols}, booktitle = {Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {11565}, pages = {192--213}, year = {2019}, } @conference{, author = {Alturki, Musab A. and Ban Kirigin, Tajana and Kanovich, Max and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn}, title = {A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols}, booktitle = {Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows}, series = {LNCS}, number = {11565}, pages = {192--213}, year = {2019}, doi = {10.1007/978-3-030-19052-1}, } @inproceedings{nigam19etfa, author = {Nigam, Vivek and Talcott, Carolyn}, title = {Formal Security Verification of Industry 4.0 Applications}, booktitle = {24th {IEEE} International Conference on Emerging Technologies and Factory Automation, {ETFA} 2019, Zaragoza, Spain, September 10-13, 2019}, publisher = {{IEEE}}, pages = {1043--1050}, year = {2019}, doi = {10.1109/ETFA.2019.8869428}, } @inproceedings{nigam19cathy, author = {Nigam, Vivek and Talcott, Carolyn and Aires Urquiza, Abra{\~{a}}o}, title = {Symbolic Timed Trace Equivalence}, booktitle = {Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {11565}, pages = {89--111}, year = {2019}, doi = {10.1007/978-3-030-19052-1\_8}, } @inproceedings{kanovich18fcs, author = {Alturki, Musab A. and Kanovich, Max and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn and Ban Kirigin, Tajana}, title = {Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols.}, booktitle = {"Workshop on Foundations of Computer Security"}, year = {2018}, abstract = {Distance-bounding (DB) protocols were proposed tothwart relay attacks on proximity-based access control systems.In a DB protocol, the verifier computes an upper bound on thedistance to the prover by measuring the time needed for a signalto travel to the prover and back. DB protocols are, however,vulnerable to distance fraud, in which a dishonest prover isable to manipulate the distance bound computed by an honestverifier. Despite their conceptual simplicity, devising a formalcharacterization of DB protocols and distance fraud attacks thatis amenable to automated formal analysis is non-trivial, primarilybecause of their real-time and probabilistic nature. In this work,we present a framework, based on rewriting logic, for formallyanalyzing different forms of distance-fraud, including recentlyidentified timing attacks. We introduce a generic, real-time andprobabilistic model of DB protocols and use it to (mechanically)verify false-acceptance and false-rejection probabilities undervarious settings and attacker models through statistical modelchecking with MAUDE and PVESTA. Using this framework,we first accurately confirm known results and then define andquantitatively evaluate new guessing-ahead attack strategies thatwould otherwise be difficult to analyze manually.}, } @inproceedings{mason17cosim, author = {Mason, Ian and Nigam, Vivek and Talcott, Carolyn and Vasconcelos De Brito, Alisson}, title = {A Framework for Analyzing Adaptive Autonomous Aerial Vehicles}, booktitle = {Software Engineering and Formal Methods - {SEFM} 2017 Collocated Workshops: DataMod, FAACS, MSE, CoSim-CPS, and FOCLASA, Trento, Italy, September 4-5, 2017, Revised Selected Papers}, pages = {406--422}, year = {2017}, abstract = {Unmanned aerial vehicles (UAVs), a.k.a. drones, are becoming increasingly popular due to great advancements in their control mechanisms and price reduction. UAVs are being used in applications such as package delivery, plantation and railroad track monitoring, where UAVs carry out tasks in an automated fashion. Devising how UAVs achieve a task is challenging as the environment where UAVs are deployed is normally unpredictable, for example, due to winds. Formal methods can help engineers to specify flight strategies and to evaluate how well UAVs are going to perform to achieve a task. This paper proposes a formal framework where engineers can raise the confidence in their UAV specification by using symbolic, simulation and statistical and model checking methods. Our framework is constructed over three main components: the behavior of UAVs and the environment are specified in a formal executable language; the UAV's physical model is specified by a simulator; and statistical model checking algorithms are used for the analysis of system behaviors. We demonstrate the effectiveness of our framework by means of several scenarios involving multiple drones.}, doi = {10.1007/978-3-319-74781-1_28}, url = {https://doi.org/10.1007/978-3-319-74781-1_28}, } @article{DBLP:journals/mscs/KanovichKNSTP17, author = {Kanovich, Max and Ban Kirigin, Tajana and Nigam, Vivek and Scedrov, Andre and Perovic, Ranko and Talcott, Carolyn}, editor = {Kr{\"{o}}ger, Torsten and Wahl, Friedrich M.}, title = {A rewriting framework and logic for activities subject to regulations}, journal = {Mathematical Structures in Computer Science}, volume = {27}, number = {3}, pages = {332--375}, year = {2017}, abstract = {Activities such as clinical investigations (CIs) or financial processes are subject to regulations to ensure quality of results and avoid negative consequences. Regulations may be imposed by multiple governmental agencies as well as by institutional policies and protocols. Due to the complexity of both regulations and activities, there is great potential for violation due to human error, misunderstanding, or even intent. Executable formal models of regulations, protocols and activities can form the foundation for automated assistants to aid planning, monitoring and compliance checking. We propose a model based on multiset rewriting where time is discrete and is specified by timestamps attached to facts. Actions, as well as initial, goal and critical states may be constrained by means of relative time constraints. Moreover, actions may have non-deterministic effects, i.e. they may have different outcomes whenever applied. We present a formal semantics of our model based on focused proofs of linear logic with definitions. We also determine the computational complexity of various planning problems. Plan compliance problem, for example, is the problem of finding a plan that leads from an initial state to a desired goal state without reaching any undesired critical state. We consider all actions to be balanced, i.e. their pre- and post-conditions have the same number of facts. Under this assumption on actions, we show that the plan compliance problem is PSPACE-complete when all actions have only deterministic effects and is EXPTIME-complete when actions may have non-deterministic effects. Finally, we show that the restrictions on the form of actions and time constraints taken in the specification of our model are necessary for decidability of the planning problems.}, doi = {10.1017/S096012951500016X}, url = {https://doi.org/10.1017/S096012951500016X}, } @article{DBLP:journals/jcs/KanovichKNST17, author = {Kanovich, Max and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn and Ban Kirigin, Tajana}, title = {Time, computational complexity, and probability in the analysis of distance-bounding protocols}, journal = {Journal of Computer Security}, volume = {25}, number = {6}, pages = {585--630}, year = {2017}, abstract = {Many security protocols rely on the assumptions on the physical properties in which its protocol sessions will be carried out. For instance, Distance Bounding Protocols take into account the round trip time of messages and the transmission velocity to infer an upper bound of the distance between two agents. We classify such security protocols as Cyber-Physical. Time plays a key role in design and analysis of many of these protocols. This paper investigates the foundational differences and the impacts on the analysis when using models with discrete time and models with dense time. We show that there are attacks that can be found by models using dense time, but not when using discrete time. We illustrate this with an attack that can be carried out on most Distance Bounding Protocols. In this attack, one exploits the execution delay of instructions during one clock cycle to convince a verifier that he is in a location different from his actual position. We additionally present a probabilistic analysis of this novel attack. As a formal model for representing and analyzing Cyber-Physical properties, we propose a Multiset Rewriting model with dense time suitable for specifying cyber-physical security protocols. We introduce Circle-Configurations and show that they can be used to symbolically solve the reachability problem for our model, and show that for the important class of balanced theories the reachability problem is PSPACE-complete. We also show how our model can be implemented using the computational rewriting tool Maude, the machinery that automatically searches for such attacks.}, doi = {10.3233/JCS-0560}, url = {https://doi.org/10.3233/JCS-0560}, }