We extend an existing symbolic protocol-verification tool with our adversary models. This is the first tool that systematically supports notions such as weak perfect forward secrecy, key compromise impersonation, and adversaries capable of state-reveal queries. In extensive case studies, we automatically find new attacks and rediscover known attacks that previously required detailed manual analysis.
Joint work with David Basin
This was joint work with Vitaliy Smirnov.
Experimental results on synthetic topologies embedded within Internet traffic traces from an ISP's backbone network indicate that our techniques (i) can localize the majority of bots with low false positive rate, and (ii) are resilient to the partial visibility arising from partial deployment of monitoring systems, and measurement inaccuracies arising from partial visibility and dynamics of background traffic.
The topology discovery algorithm we develop generalizes of the "master and dog" paradigm. Here is the story. A master rides a motorbike while his dog, running behind him, tries to get to him. If the master reduces the speed of the motorbike, then the dog come a bit closer to him. However, if the master accelerates, then the distance between the two increases. But, certainly enough, if the master stops for a sufficiently long period of time then the dog will reach eventually his master.
In our problem, the master is a graph representing the communication structure of a network. A move of the master corresponds to a modification of this graph. What makes our case different from the basic paradigm is that we have many dogs, each of them being a node in the graph. The distance between each dog and the master is represented by the difference between the physical graph and the image of it that each node constructs as soon as it gets some information about the "position" of the master. By definition, we say that a dog-node has reached the master-graph when the local image of the graph in this node corresponds exactly to the real situation of the graph.
In the case of the simple "master and dog" story, the dog reacts to the moves of the master because he can see the master. In our case, the situation is a bit more complicated. Only certain nodes can "see" certain moves of the graph. In other words, the nodes as a community get all information about the moves of the graph, but each individual node has only a partial direct access to these moves. More precisely, a node $n$ gets direct information about the modification of a link $l$ of the physical network if $n$ is the arriving node of link $l$.
Besides the limited information that it can get directly on the graph, each node can acquire more information about the graph from its neighbors (note that these neighbors changes over times as the graph evolves), which themselves either get some direct information on the graph or more information from their neighbors, and so on.
We would like to prove a result analogous to the one we have between the master and the dog, namely that the dog can reach his master if the latter stays still for a while. In our case, we shall prove that, under certain conditions, all dog-nodes can reach the master-graph if the latter stays still long enough.
In recent work, we have formalized important security requirements for e-voting systems, including coercion-resistance, verifiability, and accountability, both in the symbolic and cryptographic settings. In this talk, I will discuss these requirements informally and sketch our formal definitions. I will also present several state-of-the-art voting systems and discuss their security with respect to our security definitions. The talk does not assume any background on e-voting systems or cryptography.
This talk is based on joint work with Tomasz Truderung and Andreas Vogt (S&P 2009, CSF 2010, and CCS 2010).
In this presentation we will look at the semantics which models infinitely small clock drifts. If timed automaton is model checked using this "robust" semantics, the result of verification holds for infinitely small clock drifts and infinitely small imprecision on guards.
In this thesis, we conduct a full-fledged privacy exploration on six typical social networking sites. Our study mainly revolves around the life cycle of users? private data, which pertains to collection, procession, retention and deletion. An exhaustive comparative analysis has been undertaken to reveal a wide range of privacy risks.
To address the privacy problem incured by resource sharing, we propose an approach which adopts collaborative management to obtain a joint decision reflecting the ?general will?. Our proposed algorithm utilizes trust relations in social networks and combines it with the Condorcet preferential voting scheme. An optimiztion is further developed to improve its efficiency. Considering users might feel boresome in the case of large number of sharing resources, an inference technique is introduced to relieve user from the burden of massive manually input.
In this talk I will define this problem and introduce some basic solutions. We will assume that the attacker has collected a number of data dumps of different cards and that he can attribute some information to each dump, e.g. how many rides there are still has left.
(joint work with Ton van Deursen and Sasa Radomirovic)
In this talk I will present a novel such protocol and discuss its design and analysis.
Joint work with Feng Hao, James Heather, Dalia Khader, Steve Schneider,.....
When using the propositional semantics, ATrees and ADTrees can be seen as representation languages for Boolean functions. In this presentation, we will take a look at these two languages and try to answer the following questions: