Concurrency, Verification & Security Seminars

Unless otherwise stated, the seminars are on Wednesdays at 11.30am in room 347 of the Computing Laboratory. If you want to volunteer to give a seminar, please contact Philip Armstrong. If you would like to be reminded of forthcoming seminars, then you might like to subscribe to the concurrency mailing list by emailing concurrency-subscribe@maillist.ox.ac.uk.

Details of seminars in previous terms are available here.

Hilary Term, 2008

• Speaker: Dusko Pavlovic
• Place: Oxford University Computing Laboratory, Room 347
  
• Title: Near Field Communication and Security in Pervasive and Social Networks
• Abstract:
  

  Near Field Communication (NFC) is one of the short range technologies currently introduced in mobile phones. Besides emulating smart cards, it enables a wide range of short range applications, embedding social computation in physical space. Interesting security problems arise in many of them. With an imminent widespread deployment, NFC is an exciting application domain for some of the security research pursued at COMLAB.

  I shall outline some of the security problems and solutions arising from NFC and other pervasive computation technologies, and describe the ways in which the standard security models need to be extended, in order to accommodate reliable security proofs. The incremental approach, deriving secure protocols together with the corresponding security proofs, developed in our previous work, turns out to be more needed than ever.

• Speaker: Doina Bukur
• Place: Oxford University Computing Laboratory, Room 347
  
• Title: Secure Data Flow in a Calculus for Context Awareness
• Abstract:
  

  We present a process calculus to describe context-aware computing in an infrastructure-based Ubiquitous Computing setting. In our calculus, computing agents can provide and discover contextual information and are owners of security policies. Simple access control to contextual information is not sufficient to insure confidentiality in Global Computing, therefore our security policies regulate rights to the provision and discovery of contextual information over distributed flows of actions. A type system enforcing security policies by a combination of static and dynamic checking of mobile agents is provided, together with its type soundness.

  This is joint work with Mogens Nielsen, Department of Computer Science, University of Aarhus, Denmark

• Speaker: Bill Roscoe
• Place: Oxford University Computing Laboratory, Room 347
  
• Title: Completing CSP
• Abstract:
  

  After adding a natural new operator to CSP that is related to interrupt, we are able to show that no further operator can be required. Specifically, we define what it means for an operator to have a CSP-like operational semantics, and show that every such operator is expressible using the extended language.

  A side benefit of this is that it becomes possible to define new operators operationally, confident that they have congruent definitions over the semantic models and fit naturally into CSP's refinement framework.

• Speaker: Paulo Mateus
• Place: Oxford University Computing Laboratory, Room 347
  
• Title: A quantum fair contract signing protocol
• Abstract:
  

  We present a fair contract signing protocol without communication with a judge during the exchange phase. To this end we consider particular Werner states and assume that the agents have no control over the system decoherence. Finally, we show how to implement such Werner states with quantum tamper-proof devices and discuss some limitations and extensions of the proposed protocol.

  Joint work with J. Bouda and N. Paunkovic.

• Speaker: Rhys Newman
• Place: Oxford University Computing Laboratory, Room 347
  
• Title: TBA
• Abstract:
  

• Speaker: Chris Dilloway
• Place: Oxford University Computing Laboratory, Room 051
  
• Title: Secure Channels and Proxies
• Abstract:
  

  Security architectures often make use of secure transport protocols to protect network messages: the transport protocols provide secure channels between hosts. We present a framework for specifying secure channels and a hierarchy of specifications for secure channels. Our specifications are trace specifications: they capture a number of different confidentiality and authentication properties that secure channels might satisfy. We establish a partial order and an equivalence relation in the framework, and we use this to compare the strengths of the channels in the hierarchy.

  In the second half of the seminar we present a rather surprising result that arises from chaining secure channels through proxies. When two secure channels are chained through a proxy, the resultant channel can be stronger than either of the individual channels. However, in some cases, two seemingly secure channels can be chained to provide a channel which provides absolutely no security properties. We show how the properties of the resultant channel can be worked out from the properties of the channels to and from the proxy.

Past Seminars