FCS-PrivMod on Wednesday, July 14th

10:30‑12:30 Session 1
Chair: Tom Chothia
Location: AT LT1
10:30 Max Kanovich, Tajana Ban Kirigin, Vivek Nigam and Andre Scedrov
Progressing Collaborative Systems

Administrative processes usually involve progressing behavior: whenever a transaction is performed, it does not need to be repeated. In this paper, we build on existing models for collaborative systems with confidentiality policies. The actions in these models are \emph{balanced}, namely, they have an equal number of facts in their pre- and post-conditions. We propose the following extensions: (1) We introduce a leader who is trusted by all other agents, and (2) we allow balanced actions to update values with fresh ones. Then, to reflect the progressing behavior, we impose a restriction that (3) each instance of an action can be used at most once in a plan complying with a policy. We also impose a restriction that (4) balanced actions are allowed to change only one fact in a configuration. We then show that under the restrictions (3) and (4), the partial goal reachability problem and a related policy compliance problem are NP-hard even when actions do not involve fresh values. The same problems are PSPACE-hard if we omit restriction (3), and also PSPACE-hard when we keep both extension (2) and restriction (3). We use focused proofs in linear logic to formalize a semantics of actions that can create fresh values. Finally, we implement some examples in logic-based verification tools and model-check whether they comply with certain policies.

11:00 Abdessamad IMINE, Zeeshan Ahmed and Michael Rusinowitch
Safe and Efficient Strategies for Updating Firewall Policies

Due to the large size and complex structure of modern networks, firewall policies can contain several thousand rules. The size and complexity of these policies require automated tools providing a user-friendly environment to specify, configure and safely deploy a target policy. When activated in online mode, a firewall policy deployment is a very difficult and error-prone task. Indeed, it may result in self-Denial of

Service (self-DoS) and/or temporary security breaches. Much research has already addressed policy specification, conflict detection, and optimization but very little research is devoted to firewall policy deployment. Only recently, some researchers have proposed deployment strategies for two important classes of policy editing languages. In this paper, we show that these strategies have serious flaws leading to security breaches. Then we provide correct, efficient and safe algorithms for both classes of languages. Our experimental results show that these algorithms are fast and can be used safely even for deploying large policies.

\textbf{Keywords:} Firewall Policy Management, Firewalls, Network Security.

11:30 Hakima Ould-Slimane, Mohamed Mejri and Kamel Adi
Enforcing More Than Safety Properties by Program Rewriting: Algebraic Foundations

It has been proven that program rewriters (PR) \footnote{Program rewriting studied in this paper refers to the class of security enforcement mechanisms introduced in \cite{Computability06} and has no direct relation with rewriting theory.} are powerful security enforcement mechanisms. Especially, they can enforce more than safety properties. While valuable contributions have been dedicated to formally characterize ``Which''properties a PR mechanism can enforce, only few efforts have been spent on characterizing ``How'' a PR mechanism can enforce such properties. In this paper, we address the latter issue by providing algebraic foundations of PR enforcement. More precisely, given a program specification $P$ and a security property specification $\Phi$, we define an operator allowing the generation of a new version of $P$, denoted $P'$, satisfying $\Phi$. The generated program $P'$ behaves (with respect to trace equivalence) like $P$ except that it never violates $\Phi$. Since the operator is based on a notion of ``greatest common factor'', it is generic enough to cover programs intersection as well as properties composition. To characterize the operator, we transform the problem of generating $P'$ from $P$ and $\phi$ to a problem of solving a linear system under a given algebra; for which the solution is well-known in the literature. The paper is a non-trivial extension of our prior work \cite{Mejri08} in which we characterized PR enforcement of safety properties.

12:00 Etienne Lozes
Towards Information as Resource in Separation Logic

Separation Logic is a Hoare-Floyd proof system for programs manipulating resources, especially the heap. In this work, we investigate a new reading of the proof rules of separation logic in the setting of probabilistic concurrent programs. We understand the separating conjunction A*B as a statement of the independence, or absence of correlation, of two facts A and B, holding for disjoint subsets of the state. A permission, in Boyland's sense, on a given information then reflects the degree of privacy of this information. We introduce a toy programming language and provide an axiomatic semantics for it. We illustrate our approach on a protocol for oblivious transfer, and use our proof system to establish the adequacy and the preservation of privacy for this protocol.

14:00‑15:00 Session 2
Chair: Mark Ryan
Location: AT LT1
14:00 Bart Jacobs (Technical University Eindhoven)
Privacy and security issues in e-ticketing

The talk starts with an overview of privacy and security issues in current memory-card based e-ticketing, including the problems related to the (now broken) Mifare Classic chip (ao. in London's Oyster and the Netherlands' OV-chipcard). Next, more privacy-friendly, attribute-based alternatives will be discussed, for modern processor cards, using for instance bilinear pairings on elliptic curves.

15:30‑17:00 Session 3
Chair: Ben Smyth
Location: AT LT1
15:30 Jonathan Millen and John Ramsdell
Annotated sequence diagrams

An annotated sequence diagram (ASD) is a representation for a distributed logical computation in a system of locally communicating components, where communication between components is reliable and authenticated, but some components may have been compromised. We give a semantics for ASDs using multiset rewriting (MSR). Deduction rules specify how an ASD is compiled into a set of multiset rewrite rules. A Prolog program performs the compilation and interprets the MSR rules. With it, we can perform some rudimentary model checking to establish claimed properties of a system design or catch logical errors. We can also examine the consequences of malicious corruption of components. The approach is being applied to chain-of-trust arguments in a trusted platform design.

16:00 Ralf Kuesters, Henning Schnoor and Tomasz Truderung
A Formal Definition of Online Abuse-freeness

Abuse-freeness is an important security property required for contract-signing protocols. In previous work, Kaehler, Kuesters, and Wilke proposed a definition for offline abuse-freeness. In this work, we generalize this definition to online abuse-freeness and apply it to two prominent contract-signing protocols. We demonstrate that online abuse-freeness is strictly stronger than offline abuse-freeness.

16:30 SARR Augustin P., Elbaz--Vincent Philippe and Bajard Jean--Claude
Enhanced Security and Efficiency for Authenticated Key Agreement

The Canetti--Krawczyk (CK) and extended Canetti--Krawczyk (eCK) security models, are widely used to provide security arguments for key agreement protocols. We discuss shades in the (e)CK models, which make practical attacks unconsidered in security arguments. We propose a strong security model encompasses the eCK one. We propose a new protocol, called Strengthened MQV (SMQV), which in addition to provide the same efficiency as the (H)MQV protocols, is particularly suited for distributed implementations wherein a tamper--proof device is used to store long--lived keys, while session keys are used on an untrusted host machine. The SMQV protocol meets the strong security definition under the Gap Diffie--Hellman assumption and the Random Oracle model.