Latest Work

• 

  Towards the Automated Verification of Cyber-Physical Security Protocols: Bounding the Number of Timed Intruders*

  Timed Intruder Models have been proposed for the verification of Cyber-Physical Security Protocols (CPSP) amending the traditional Dolev-Yao intruder to obey the physical restrictions of the environment. Since to learn a message, a Timed Intruder needs to wait for a message to arrive, mounting an attack may depend on where Timed Intruders are. It may well be the case that in the presence of a great number of intruders there is no attack, but there is an attack in the presence of a small number of well placed intruders. Therefore, a major challenge for the automated verification of CPSP is to determine how many Timed Intruders to use and where should they be placed. This paper answers this question by showing it is enough to use the same number of Timed Intruders as the number of participants. We also report on some preliminary experimental results in discovering attacks in CPSP.

  Continue Reading »

• 

  Can we mitigate the attacks on Distance-Bounding Protocols by using challenge-response rounds repeatedly?*

  In our previous work, we discovered a new attack on Distance Bounding Protocols, called AttackIn-Between-Ticks, showing that an Intruder can gain access to a resource although he is not within the pre-established distance to Verifier. The attack exploits the differences between discrete measurements used by Verifier and the actual distance. We then speculated that the Attack in Between Ticks could be mitigated by using a large number of challenge response rounds.This paper works out the details building the formal machinery to support this idea. We obtain some surprising (non-intuitive)results. We show that in the case where Verifier decides to grant theaccess by the simple majority, the effect of the repeated challenge responserounds can mitigate the attack but only for the specificvalues of the probability of the erroneous decision in one round.Whereas in the case where Verifier decides to grant the accessby the large majority (that is, with gaining a large specifiedlevel of support, for example, Prover responding in time in twothirds of the challenges) the idea of repeated challenge-responserounds works perfectly well for our protocol.

  Continue Reading »

• 

  Formal Specification and Analysis of Robust Adaptive Distributed Cyber-Physical Systems*

  We are interested in systems of cyber-physical agents that operate inunpredictable, possibly hostile, environments using locally obtainable information.How can we specify robust agents that are able to operate alone and/or incooperation with other agents? What properties are important? How can they beverified?In this tutorial we describe a framework called Soft Agents, formalized in theMaude rewriting logic system. Features of the framework include: explicit representationof the physical state as well as the cyber perception of this state; robustcommunication via sharing of partially ordered knowledge, and robust behaviorbased on soft constraints. Using Maude functionality, the soft agent frameworksupports experimenting with, formally testing, and reasoning about specificationsof agent systems.The tutorial begins with a discussion of desiderata for soft agent models. Use ofthe soft agent framework for specifcation and formal analysis of agent systemsillustrated in some detail by a case-study involving simple patrolling bots. A morecomplex case study involving surveillance drones is also discussed.

  Continue Reading »