The AVISPA Tool is a push-button tool for the Automated Validation of Internet Security Protocols and Applications. It provides modular expressive formal language specifying protocols their security properties, integrates different back-ends that implement variety automatic protocol analysis techniques. Experimental results, carried out on large library protocols, indicate state-of-the-art as, to our knowledge, no other exhibits same level scope robustness while enjoying performance scalability.

Temporal role based access control models support the specification and enforcement of several temporal constraints on enabling, activation, hierarchies among others. In this paper, we define three mappings that preserve solutions to a class policy problems (they map security analysis in presence static without them) show how they can be used extend capabilities tool for administrative role-based policies reason hierarchies. An experimental evaluation with prototype implementation shows...

We apply formal methods to lay and streamline theoretical foundations reason about Cyber-Physical Systems (CPSs) cyber-physical attacks. focus on integrity DoS attacks sensors actuators of CPSs, the timing aspects these Our contributions are threefold: (1) we define a hybrid process calculus model both CPSs (2) threat provide means assess attack tolerance/vulnerability with respect given attack. (3) formalise how estimate impact successful CPS investigate possible quantifications success...

We apply formal methods to lay and streamline theoretical foundations reason about Cyber-Physical Systems (CPSs) physics-based attacks, i.e., attacks targeting physical devices. focus on a treatment of both integrity denial service sensors actuators CPSs, the timing aspects these attacks. Our contributions are fourfold. (1) define hybrid process calculus model CPSs (2) formalise threat that specifies MITM can manipulate sensor readings or control commands drive CPS into an undesired state;...

In 2017, the Defense Advanced Research Projects Agency (DARPA) launched Explainable Artificial Intelligence (XAI) program that aims to create a suite of new AI techniques enable end users understand, appropriately trust, and effectively manage emerging generation systems. this paper, inspired by DARPA's XAI program, we propose paradigm in security research: Security (XSec). We discuss "Six Ws" XSec (Who? What? Where? When? Why? How?) argue has unique complex characteristics: involves several...

User identification procedures, essential to the information security of systems, enable system-user interactions by exchanging data through communication links and interfaces validate confirm user authenticity. However, human errors can introduce vulnerabilities that may disrupt intended workflow thus impact system behavior. Therefore, ensuring integrity these procedures requires accounting for such erroneous behaviors. We follow a formal, human-centric approach analyze modeling them as...

We introduce constraint differentiation, a powerful technique for reducing search when model-checking security protocols using constraint-based methods. Constraint differentiation works by eliminating certain kinds of redundancies that arise in the space constraints to represent nd manipulate messages may be sent an active intruder. define general way, independent technical and conceptual details underlying method protocol model. Formally, we prove terminates is correct, under assumption...

Vertical composition of security protocols means that an application protocol (e.g., a banking service) runs over channel established by another secure provided TLS). This naturally gives rise to compositionality question: given P1 provides certain kind as goal and P2 assumes this channel, can we then derive their vertical P2[P1] is secure? It well known lead attacks even when the individual are all in isolation. In paper, formalize seven easy-to-check static conditions support large class...

We introduce constraint dieren tiation, a new technique for reducing search when modelchecking security protocols. Our is based on eliminating certain kinds of redundancies that arise in the space using symbolic exploration methods, particular methods employ constraints to represent and manipulate possible messages from an active intruder. Formally, we prove tiation terminates correct complete, it preserves set reachable states so all state-based properties holding before reduction (such as...

Journal Article Relating Strand Spaces and Distributed Temporal Logic for Security Protocol Analysis Get access Carlos Caleiro, Caleiro Search other works by this author on: Oxford Academic Google Scholar Luca Viganò, Viganò David Basin of the IGPL, Volume 13, Issue 6, November 2005, Pages 637–663, https://doi.org/10.1093/jigpal/jzi048 Published: 01 2005