Alice and Bob notation is a popular way to describe security protocols: it intuitive, succinct, yet expressive. Several formal protocol specification languages are based on this notation. One of the most severe limitations these lack algebraic reasoning, which required for instance correct interpretation Diffie-Hellman protocols. As consequence, previous approaches either cannot handle such protocols at all or require manual annotation. We generalize give first semantics language that...

The pervasiveness of cloud computing can be attributed to its scale and elasticity. However, the operational complexity underlying infrastructure is high, due dynamics, multi-tenancy, size. Misconfigurations insider attacks carry significant security risks, such as breaches in tenant isolation put both provider consumers at risk.

The abstraction and over-approximation of protocols web services by a set Horn clauses is very successful method in practice. It has however limitations for that are based on databases keys, contracts, or even access rights, where revocation possible, so the true facts does not monotonically grow with state transitions. We extend scope these methods defining new way can handle such databases, we formally prove sound. realize translator from convenient specification language to standard use...

We address the problem of privacy-preserving access control in distributed systems. Users commonly reveal more personal data than strictly necessary to be granted online resources, even though existing technologies, such as anonymous credential systems, offer functionalities that would allow for privacy-friendly authorization. An important reason this lack technology adoption is, we believe, absence a suitable authorization language offering adequate expressiveness functionalities. To...

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...

The security of key exchange and secure channel protocols, such as TLS, has been studied intensively. However, only few works have considered what happens when the established keys are actuallyused -- to run some protocol securely over "channel". We call this a vertical composition, it is truly commonplace in today's communication with diversity VPNs browser sessions. In fact, normal that we several layers channels: For instance, on top VPN-connection, may establish another (possibly...

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...

Virtualized infrastructures and clouds present new challenges for security analysis formal verification: they are complex environments that continuously change their shape, give rise to non-trivial goals such as isolation failure resilience requirements. We a platform connects declarative expressive description languages with state-of-the art verification methods. The integrate homogeneously descriptions of virtualized infrastructures, transformations, desired goals, evaluation strategies....

We introduce CDiff, a new technique for reducing search when model-checking 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 CDiff terminates correct complete, it preserves set reachable states so all state-based properties holding before reduction (such as intruder discovering...

Communication protocols often rely on stateful mechanisms to ensure certain security properties. For example, counters and timestamps can be used authentication, or the of communication depend whether a particular key is registered server it has been revoked. ProVerif, like other state art tools for protocol analysis, achieves good performance by converting formal specification into set Horn clauses, that represent monotonically growing facts Dolev-Yao attacker derive from system. Since this...