SECURITY (OLD) SEMINARS -------------------------------- Date and time: Tuesday 28th July 2009 at 11:00 Location: 124, School of Computer Science Title: A formal framework for quantifying voter-controlled privacy. Speaker: Hugo Jonker (http://satoss.uni.lu/members/hugo/) Abstract: Privacy is a necessary requirement for voting. Without privacy, voters can be forced to vote in specific ways, and the forcing party can check their compliance. But offering privacy does not suffice: if a voter can reduce her privacy, an attacker can force her to do so. In this presentation, we distinguish various ways that a voter can communicate with the intruder to reduce her privacy and classify them according to their ability to reduce the privacy of a voter. We develop a framework combining knowledge reasoning and trace equivalences to formally model voting protocols and define voter-controlled privacy. Our framework is quantitative, in the sense that it defines a measure for the privacy of a voter. Therefore, the framework can precisely measure the level of privacy for a voter for each of the identified privacy-reduction classes. The quantification allows our framework to capture receipts that reduce, but not nullify, the privacy of the voter. -------------------------------- Date and time: Tuesday 28th July 2009 at 15:00 Location: 245, School of Computer Science Title: Automated reasoning for election verifiability in electronic voting protocols Speaker: Ben Smyth (http://www.cs.bham.ac.uk/~bas/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: TBC -------------------------------- Date and time: Friday 7th August 2009 at 12:00 Location: 245, School of Computer Science Title: Analysis of the e-passport RFID protocol. Speaker: Tom Chothia (http://www.cs.bham.ac.uk/~tpc/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: I will discuss the protocols used by the RFID chips in passports. As passports are often carried on the user, new kinds of attacks are possible. I will outline an appropriate attacker model and review some related work. I will then present some new analysis of the security these passports offer. -------------------------------- Date and time: Thursday 1st October 2009 at 11:00 Location: 245, School of Computer Science Title: A Research Review on Multi-signatures Provably Secure in the Plain Public Key Model Speaker: Dr. Wei Gao Abstract: Abstract: A multi-signature scheme is a special kind of digital signature in which a group of signers can jointly produce a compact signature on the same message. It has many potential use, for example, contract signing, co-signing, and distribution of a certificate authority. In this talk, I will introduce this research topic in the framework of provably secure cryptography. First, I will present the framework by giving the security definition of multi-signature. In other words, I will formally define what is a provably secure multi-signature scheme in the plain public key model. Second, I will review the main results in this topic including naive multi-signature scheme, Bellare-Neven multi-signature (BN2006), Ma-Weng-Li-Deng multi-signature (MWLD 2009), Bagherzandi-Cheon-Jarecki multi-signature (BCJ2008), and Le-Bonnecaze-Gabillon multi-signature(LBG 2009). I will highlight the main ideas underlying each scheme and their relations. At last, I will present our further research in the future, especially our main idea on analysing and constructing multi-signature scheme. Reference: [BN2006] BellareM., Neven G.: Multi-signature in the plain public-key model and a genral forking lemma. In: The 13th ACM Conference on Computer and Communication Security (2006). [MWLD 2009] Changshe Ma, Jiang Weng, Yingjiu Li, Robert Deng. : Efficient discrete logarithm based multi-signature scheme in the plain public key model. Designs, Codes and Crytography. To appear. DOI 10.1007/s10623-009-9313-z [BCJ2008] Bagherzandi A., Cheon J.H., Jarecki S.: Multisignatures secure under the discrete logarithm assumption and a generalized forking lemma. In: The 15th ACM Conference on Computer and Communication Security (2008). [LBG 2009] Duc-Phong Le, Alexis Bonnecaze, Alban Gabillon: Multisignatures as Secure as the Diffie-Hellman Problem in the Plain Public-Key Model. Pairing 2009. Springer LNCS 5671, pp. 35-51 -------------------------------- Date and time: Thursday 15th October 2009 at 11:00 Location: 245, School of Computer Science Title: Challenges in electronic voting: the case of Prêt à Voter Speaker: Sergiu Bursuc (http://www.lsv.ens-cachan.fr/~bursuc/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: Voting is one of the many activities that nowadays tend to become electronic. This for good reason, since electronic voting not only promises improvement of participation rate or economies in the overall process of voting. It opens also the possibility for other desirable properties, that are hard to imagine in the context of traditional elections: for instance, the ability of a voter to verify that his vote has been really counted. However, when going online things get delicate and promised properties hide subtle flaws, or assumptions that might not be met in practice. This makes the rigorous design and analysis of electronic voting protocols an important and challenging task. In this talk, I will present design principles, possible threats and fixes for Pret A Voter - an electronic voting system that tries to ensure both vote verifiability and coercion resistance. Much work remains to be done to achieve a high degree of confidence and public acceptance of Pret A Voter, or any other voting system. On the design side, we need to use less paper (zero) and simpler, cheaper devices. On the analysis side, we need a precise modelling of possible threats and formal, automatic verification of protocol correctness. Obviously, the problem is the more interesting as these two goals are potentially contradictory. -------------------------------- Date and time: Thursday 12th November 2009 at 11:00 Location: 245, School of Computer Science Title: Remote Electronic Voting with Revocable Anonymity Speaker: Matthew Smart (http://www.cs.bham.ac.uk/~mjs/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: We present a new remote, coercion-free electronic voting protocol which satisfies a number of properties previously considered contradictory. We introduce (and justify) the idea of revocable anonymity in electronic voting, on the grounds of it being a legal requirement in the United Kingdom, and show a method of proving the validity of a ballot to a verifier in zero knowledge, by extension of known two-candidate proofs. -------------------------------- Date and time: Thursday 19th November 2009 at 11:00 Location: 245, School of Computer Science Title: A new attack on SSL Speaker: Tom Chothia (http://www.cs.bham.ac.uk/~tpc/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: Tom will present a recently discovered attack on the SSL protocol. -------------------------------- Date and time: Thursday 26th November 2009 at 11:00 Location: 245, School of Computer Science Title: Deducibility constraints in a quotient algebra: reduction of models and applications to security Speaker: Sergiu Bursuc (http://www.lsv.ens-cachan.fr/~bursuc/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: To enable formal and automated analysis of security protocols, one has to abstract implementations of cryptographic primitives by terms in a given algebra. However, the algebra can not be free, as cryptographic primitives have algebraic properties that are either relevant to their specification or else they can be simply observed in implementations at hand. These properties are sometimes essential for the execution of the protocol, but they also open the possibility for an attack, as they give to an intruder the means to deduce new information from the messages that he intercepts over the network. In consequence, there was much work over the last few years towards enriching the Dolev-Yao model, originally based on a free algebra, with algebraic properties, modelled by equational theories. In this context, we have been interested in general decision procedures for the insecurity of protocols, that can be applied to classes of equational theories. First, we propose a general way to simplify an equational theory, based on an appropriate definition of alien subterms of a term. From this, we derive a decision procedure for a non-trivial combination of Abelian group properties, exponentiation and homomorphism. This theory was used for modelling an electronic purse protocol by France Telecom. Previously known techniques were not applicable, as the theory was a too intricate combination of sub-theories. Next, we show that constraint systems, that represent all possible traces of a protocol, can be simplified in an uniform and systematic way, when the equational theory does not contain Associative-Commutative symbols. This allows for a symbolic representation of all traces of a protocol as a set of solved forms. The main property of the equational theory that ensures the completeness of the proposed simplification procedure is saturation with respect to ordered resolution. When the saturated theory is finite, the set of solved forms is finite as well and permits deciding any trace property, in particular the secrecy of a message. When the saturated theory is infinite, one needs to group solved forms together, by introducing a new predicate, in order to obtain a finite representation of all solutions of the original system. This has been done for the particular case of blind signatures and is yet to be understood in a more general setting. -------------------------------- Date and time: Thursday 3rd December 2009 at 11:00 Location: 245, School of Computer Science Title: A Designated Confirmer Signature from Bilinear Maps Speaker: Fubiao Xia (http://www.cs.bham.ac.uk/about/people/showperson.php?person_id=4653) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: After the introduction of designated confirmer signatures by Chaum at Eurocrypt 1994, a lot of research work have been made to build generic schemes from standard digital signatures, or construct efficient concrete schemes. In designated confirmer signature schemes, a signature can be verified only with the help of a semi-trusted third party, called the designated confirmer. If necessary, the confirmer can publicly reveal its validity by converting the designated confirmer signature into an ordinary signature. However, most of the existing schemes are either inefficient or insecure. In this talk, I will introduce a new designated confirmer signature scheme based on bilinear maps, which has been proved security in random oracle model. We find a new feature that both the signer and the designated confirmer can convince or disavow a signature, while the signer does not possess the disavow ability in all previous schemes. -------------------------------- Date and time: Friday 1st January 2010 at 13:00 Location: 245, School of Computer Science Title: Automating security analysis: symbolic equivalence of constraint systems Speaker: Sergiu Bursuc Institution: School of Computer Science, University of Birmingham Abstract: Security protocols are dynamic in nature: the output of participating agents depends on the messages that they receive from the environment. This entails that the set of possible executions of a given protocol, also called its set of traces, is infinite. When one aims to verify that a protocol is correct, one has to prove that this set of traces satisfies a certain security property. Therefore, the fact that the number of traces is infinite makes protocol verification a challenging theoretical problem. A constraint system is a finite representation of the infinite set of traces of a protocol that can be used as a symbolic data structure in a verification algorithm. The first goal of my talk is to introduce constraint systems and explain their importance by relevant examples. In the second part of my talk, I will show a verification algorithm based on constraint systems. Namely, I will show how in certain cases observational equivalence of processes, that formalizes security properties such as privacy preservation, can be decided using constraint systems. The talk is based on the paper with the same title by Vincent Cheval, Hubert Comon-Lundh and Stephanie Delaune. -------------------------------- Date and time: Thursday 21st January 2010 at 11:00 Location: 245, School of Computer Science Title: Train Station Ticket Barriers: Do they work? Speaker: Christopher Staite (http://www.cs.bham.ac.uk/~cxs548/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: After the installation of ticket barriers at local stations, I have been looking into their capabilities and limitations. Myself, Tom and Matt have been trying to read the tickets and in turn learn how the system may be exploited. Our results are currently inconclusive, but we have learnt many details and hope to explore more avenues of investigation. In this talk a summary of the information that has been gathered thus far will be given. This will compare the barriers installed locally to those in London. Additionally, the technical issues we have encountered will be discussed in the hope of input in order to overcome them. -------------------------------- Date and time: Thursday 28th January 2010 at 11:00 Location: 245, School of Computer Science Title: A Framework for Broadcast Authentication in Wireless Sensor Networks Speaker: Rehana Yasmin Institution: School of Computer Science, University of Birmingham Abstract: Although symmetric key cryptography is efficient in processing for resource constrained sensor nodes, it is not able to solve all security issues in Wireless Sensor Network (WSN). In broadcast authentication, where all potential receivers share a single Message Authentication Code (MAC) key to authenticate messages from a sender, any compromised receiver can forge messages on behalf of the sender. Furthermore, Message Authentication Code does not provide source authentication in broadcast scenario. Digital signatures are used in traditional networks to authenticate messages. However, asymmetric cryptography increases processing time and energy consumption on sensor nodes. Public keys and certificates management is another issue with asymmetric cryptography. To handle this problem, we propose an authentication framework using Identity-based Online/Offline Signatures. Identity-based cryptography solves the problem of public keys and certificates management. Online/Offline signatures allow to perform complex computations of signature generation on resourceful devices to reduce computation time and energy consumption on sensor nodes. -------------------------------- Date and time: Thursday 25th February 2010 at 11:00 Location: 245, School of Computer Science Title: Knowledge based verification of access control policies through alternating-time temporal logic (ATL) Speaker: Masoud Koleini (http://www.cs.bham.ac.uk/~mxk815/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) Abstract: Alternating time temporal logic (ATL) is a branching-time temporal logic that describes multi-agent systems and is based on game theory. Concurrent systems, which consist of collection of interacting agents can be described in ATL logic. The state transition of the system is based on the concurrent actions of the agents and the strategy will be a sequence of concurrent actions in the system for achieving the coalition of agents to the goal. Reasoning about the activities in a system, which is known as the "knowledge", is one of the important concepts in multi-agent distributed systems, which could be also included in ATL. In the presentation, I will talk about ATL logic specifications and introduce a model-checker for ATL logic (MCMAS), which is also capable of reasoning about agents knowledge. Then I will discuss how access control policies can be translated into MCMAS syntax for the verification and reasoning about knowledge. At the end, I will have a discussion about the practical limitations of ATL model-checkers. -------------------------------- Date and time: Tuesday 2nd March 2010 at 12:00 Location: 245, School of Computer Science Title: Mitigate Unauthorized Tracking in RFID Discovery Service Speaker: Dr. Tieyan Li (http://icsd.i2r.a-star.edu.sg/staff/tieyan/) Institution: Institute for Infocomm Research (Singapore) (http://icsd.i2r.a-star.edu.sg/) Host: School of Computer Science, University of Birmingham Abstract: One of the most important privacy concerns in RFID-enabled supply chain management systems is unauthorized tracking of RFID tagged assets, which may take place at the physical level or the system level. Prior research has focused on the prevention of clandestine scanning at the physical level, where an adversary uses an unauthorized reader collecting RF waves to track the movement of RFID tags. However, the threat of unauthorized tracking at the system level, where an adversary tracks movement of RFID tagged assets by eavesdropping network messages or compromising date center servers, has not been well recognized in the literature. Compared to the former, the latter could be even more harmful as the adversary is able to obtain tracking information on a global scale and without physical presence. RFID Discovery Service, as specified in the current industrial standard EPCglobal Network, is a restricted-access database for depositing RFID tag location records. In this talk, we analyze the threat of unauthorized tracking by a semi-trusted Discovery Service and propose a pseudonym-based design to mitigate the threat. Our design protects against Discovery Service database reading attack and provides efficient key management and access control. The design is backward compatible with the existing communication protocols and database schemas of RFID Discovery Service, which makes it feasible to deploy in real applications. Biography: Dr. Tieyan Li is a senior research fellow at Institute for Infocomm Research (Singapore). He obtained his Ph.D. degree at School of Computing, National University of Singapore. Dr. Li is experienced in practical system developments and also active in academic security research fields with tens of journal and conference publications and several patents. Currently his areas of research are in applied cryptography and network security, as well as security issues in RFID, sensor, multimedia and tamper resistant hardware/software, etc. Dr. Li has served as the PC member and reviewer for a number of security conferences and journals. -------------------------------- Date and time: Thursday 11th March 2010 at 11:00 Location: 245, School of Computer Science Title: Automatic abstraction and refinement method for state-based access control system verification Speaker: Masoud Koleini (http://www.cs.bham.ac.uk/~mxk815/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) Abstract: The model-checkers suffer from state explosion problem when the number of variables grows in the system. Incrementing the number of variables causes the number of states in the system to grow exponentially. Abstraction is one of the most important methods which reduces the states of the original system in such a way it can be analysed by regular model-checkers. In the presentation, I will discuss the theory behind abstraction and talk about CEGAR (counter-example guided abstraction refinement) framework. I will discuss a method based on variable hiding abstraction and then describe the counter-example-based refinement for it. At the end, I will simulate an access control scenario on MCMAS model-checker (model-checker for multi-agent systems) and demonstrate how this method can reduce the amount of time and space in the verification. -------------------------------- Date and time: Friday 12th March 2010 at 13:00 Location: 245, School of Computer Science Title: An Introduction to Zero Knowledge proofs Speaker: Dr. Yi Deng Abstract: Zero knowledge proof, introduced by Goldwasser et al. in 1985, allows one player (called the Prover) to convince another player (the Verifier) of the truth of a mathematical statement, without revealing anything else to the Verifier. In this talk, we will give an introduction to zero knowledge proof and explain some key ideas behind this concept and its application to cryptography. Also, we will talk about zero knowledge protocols in some malicious (but realistic) communication settings, such as the concurrent and resettable setting, and survey some recent results in these fields. BIOGRAPHY Yi Deng received his Ph.D. in cryptography from Institute of Software, Chinese Academy of Sciences (CAS) in 2008. From Feb. 2008 to May 2009, he was an assistant researcher at State key laboratory of infomation security, CAS; In June 2009 he joined UCL as an associate researcher. His research interest lies in theory of cryptography, especially zero knowledge and pseudorandomness. He has published several papers at venues such as Eurocrypt and FOCS. -------------------------------- Date and time: Thursday 15th April 2010 at 10:00 Location: 245, School of Computer Science Title: An Overview of Wi-Fi security Speaker: Warren Prescott Institution: School of Computer Science, University of Birmingham Host: Tom Chothia -------------------------------- Date and time: Thursday 15th April 2010 at 10:30 Location: 245, School of Computer Science Title: Common Hacking Techniques Speaker: Matthew Wilkinson Institution: School of Computer Science, University of Birmingham Host: Tom Chothia -------------------------------- Date and time: Thursday 20th May 2010 at 11:00 Location: 124, School of Computer Science Title: Framework for trust monitoring and prediction Speaker: Olufunmilola Onolaja (http://www.cs.bham.ac.uk/~ooo668/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) Abstract: In this talk we present a conceptual framework for reputation and trust based systems for mobile adhoc networks. These networks have been plagued with internal security issues such as the presence of untrusted nodes that misbehave. Depending on the proportion of misbehaving nodes and their strategies, attacks such as collusions may occur. By covering up malicious behaviour of one another from the remaining part of the network, two or more malicious nodes may collaborate to cause damage to or disrupt the network. The framework exploits the dynamic data driven application systems paradigm and is potentially able to improve on the security of such networks. -------------------------------- Date and time: Thursday 3rd June 2010 at 11:00 Location: 245, School of Computer Science Title: The Challenge of Privacy in VANETs Speaker: Loretta I. Mancini Institution: School of Computer Science, University of Birmingham Abstract: Vehicular Ad-hoc Networks (VANETs) will enable vehicle-to-vehicle and vehicle-to-road infrastructure communication aiming to support road safety and enhance driving experience. Many frameworks and applications have been proposed in literature so far. However the security of VANETs is critical for their deployment. In fact, VANETs' peculiar characteristics make traditional security enforcement techniques inadequate in many cases. In particular one of the most challenging issues concerns the trade-off between the privacy of drivers and the accountability of misbehaving vehicles. In this talk we will present an overview of VANETs and some of the work available in the literature addressing the challenge of ensuring privacy in VANETs. -------------------------------- Date and time: Thursday 10th June 2010 at 11:00 Location: 245, School of Computer Science Title: Modelling Dynamic Access Control Policies for Web-Based Collaborative Systems Speaker: Hasan Qunoo (http://www.cs.bham.ac.uk/~hxq/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) Abstract: We present a modelling language, called X-Policy, for webbased collaborative systems with dynamic access control policies. The access to resources in these systems depends on the state of the system and its configuration. The X-Policy language models systems as a set of actions. These actions can model system operations which are executed by users. The X-Policy language allows us to specify execution permissions on each action using complex access conditions which can depend on data values, other permissions, and agent roles. We demonstrate that X-Policy is expressive enough to model collaborative conference management systems. We model the EasyChair conference management system and we reason about three security attacks on EasyChair. -------------------------------- Date and time: Thursday 17th June 2010 at 11:00 Location: 245, School of Computer Science Title: Introduction to denotational semantics Speaker: Dan Ghica (http://www.cs.bham.ac.uk/~drg) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) Abstract: I will explain what denotational semantics is, contrast it with operational semantics and illustrate this difference with some concrete examples of reasoning about properties of particular programs. -------------------------------- Date and time: Thursday 24th June 2010 at 11:00 Location: 245, School of Computer Science Title: Privacy-supporting cloud-based collaborative systems: a formal model and a case study Speaker: Sergiu Bursuc Institution: School of Computer Science, University of Birmingham Abstract: Cloud computing raises privacy and confidentiality concerns because the service provider necessarily has access to users' data, and could accidentally or deliberately disclose it. We show that, for a significant class of systems, the requirement of cloud-side data processing is small enough that it is possible to use client-side encryption on the sensitive data, while revealing just enough insensitive data to the cloud provider to enable it to perform the required processing. We use as an example a cloud-based conference management system. We describe a privacy-preserving protocol in which authors, reviewers and the conference chair interact through their web browsers with the cloud, to perform the usual tasks of uploading and downloading papers and reviews. We specify fine-grained privacy policies expressing the cloud provider's inability to link scores with papers, reviews with authors, etc. We describe our protocol in a process calculus and informally argue that the protocol satisfies the privacy policies. -------------------------------- Date and time: Tuesday 29th June 2010 at 11:00 Location: 217, School of Computer Science Title: Automated verification of selected equivalences for synchronous cryptographic protocols Speaker: Ben Smyth (http://www.bensmyth.com/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) Abstract: A new automated method for the analysis of cryptographic protocols is delivered with a particular focus on schemes that require participants to synchronise their actions in a specific manner. This pre-requisite is typical amongst privacy preserving systems, for example: electronic voting protocols, Direct Anonymous Attestation schemes, and anonymity networks. Our contribution is as follows: we extend the applied pi calculus to allow such protocols to be modelled;develop automated reasoning techniques for equivalence; and prove the results are sound. It follows immediately from this work that a larger class of equivalences can be mechanically analysed. Furthermore, the applicability of the result is demonstrated by providing the first automated analysis of privacy in the electronic voting protocol FOO. For those familiar with ProVerif, this talk will help avoid the situation whereby ProVerif fails to prove equivalence that take the form out(c,diff[M,N]) | out(c,diff[N,M]) and of course more complex variants. -------------------------------- Date and time: Thursday 1st July 2010 at 11:00 Location: 217, School of Computer Science Title: Automated verification of selected equivalences for synchronous cryptographic protocols Speaker: Ben Smyth (http://www.bensmyth.com/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) Abstract: A new automated method for the analysis of cryptographic protocols is delivered with a particular focus on schemes that require participants to synchronise their actions in a specific manner. This pre-requisite is typical amongst privacy preserving systems, for example: electronic voting protocols, Direct Anonymous Attestation schemes, and anonymity networks. Our contribution is as follows: we extend the applied pi calculus to allow such protocols to be modelled;develop automated reasoning techniques for equivalence; and prove the results are sound. It follows immediately from this work that a larger class of equivalences can be mechanically analysed. Furthermore, the applicability of the result is demonstrated by providing the first automated analysis of privacy in the electronic voting protocol FOO. For those familiar with ProVerif, this talk will help avoid the situation whereby ProVerif fails to prove equivalence that take the form out(c,diff[M,N]) | out(c,diff[N,M]) and of course more complex variants. -------------------------------- Date and time: Tuesday 27th July 2010 at 14:00 Location: 124, School of Computer Science Title: Secure and Privacy Aware Wireless Systems: Low Resource Cryptography Primitives a Key Enabler Speaker: Mohammed Benaissa (http://www.sheffield.ac.uk/eee/staff/m_benaissa.html) Institution: University of Sheffield (http://www.sheffield.ac.uk/eee/) Abstract: The proliferation of pervasive technologies such as RFID and Wireless Sensor Networks raises the stakes in terms of both security and privacy concerns. From the engineering perspective, the issues translate into the challenging trade-off of Security versus Privacy versus Low-resource versus Real-time operation. In this talk, I will start by advocating a holistic approach to address the above challenge; researchers in this area have tended to focus on a single aspect of the trade-off at a time. In the approach, security and privacy are investigated concurrently at all levels (protocol, primitives, and physical) under a range of practical constraints, dictated by intended usage, to enable any weaknesses at a given level to be addressed at another. I will focus on the importance of the low resource implementation of strong cryptography primitives as a key enabler in the holistic approach and will present a detailed case study (from protocol to prototyping) in the context of the extreme case of a low frequency ( 125 kHz) passive (battery-less) RFID. I will also touch on the important issue of scalability and present some recent work on scalable low resource elliptic curve cryptography processors. -------------------------------- Date and time: Friday 30th July 2010 at 11:00 Location: 245, School of Computer Science Title: Verifying security property of P2P systems using CSP Speaker: Tien Tuan Anh Dinh (http://www.cs.bham.ac.uk/~ttd/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) -------------------------------- Date and time: Tuesday 3rd August 2010 at 11:00 Location: 245, School of Computer Science Title: Programming in the horn clause language of ProVerif (motivation and challenges) Speaker: Mark Ryan (http://www.cs.bham.ac.uk/~mdr) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) Abstract: Systems that involve persistent state (such as RFID tags and the TPM) are difficult to model in ProVerif's process calculus input language because of the abstractions that ProVerif makes. I will explain how ProVerif translates its process calculus input to Horn clauses, and how it reasons on the clauses. I will talk about my attempts to program directly using the Horn clause input language, in order to overcome its limitations with persistent state. This is work in progress. -------------------------------- Date and time: Monday 9th August 2010 at 14:00 Location: 245, School of Computer Science Title: SSH: Breaking and Provably Repairing a Secure Network Protocol Speaker: Gaven Watson (http://www.isg.rhul.ac.uk/~mqah080/) Institution: Royal Holloway, University of London (http://www.isg.rhul.ac.uk/) Abstract: In this talk we present a variety of plaintext-recovery attacks against SSH. We show why a combination of flaws in the basic design of SSH leads implementations such as OpenSSH to be open to our attacks and why the previous provable security results for SSH by Bellare et al. did not cover our attacks. Following this we present a new formal security analysis of SSH in counter mode in a security model that accurately captures the capabilities of real-world attackers, as well as security-relevant features of the SSH specifications and the OpenSSH implementation of SSH. This new analysis helps to bridge the gap between the existing security analysis of SSH by Bellare et al. and our attacks which partially invalidate that analysis. -------------------------------- Date and time: Thursday 21st October 2010 at 11:00 Location: 245, School of Computer Science Title: Automating security analysis: symbolic equivalence of constraint systems Speaker: Sergiu Bursuc Institution: School of Computer Science, University of Birmingham Abstract: Security protocols are dynamic in nature: the output of participating agents depends on the messages that they receive from the environment. This entails that the set of possible executions of a given protocol, also called its set of traces, is infinite. When one aims to verify that a protocol is correct, one has to prove that this set of traces satisfies a certain security property. Therefore, the fact that the number of traces is infinite makes protocol verification a challenging theoretical problem. A constraint system is a finite representation of the infinite set of traces of a protocol that can be used as a symbolic data structure in a verification algorithm. The first goal of my talk is to introduce constraint systems and explain their importance by relevant examples. In the second part of my talk, I will show a verification algorithm based on constraint systems. Namely, I will show how in certain cases observational equivalence of processes, that formalizes security properties such as privacy preservation, can be decided using constraint systems. The talk is based on the paper with the same title by Vincent Cheval, Hubert Comon-Lundh and Stephanie Delaune. -------------------------------- Date and time: Thursday 4th November 2010 at 11:00 Location: 245, School of Computer Science Title: Title: A cursory look at CHAM Speaker: Dan Ghica (http://www.cs.bham.ac.uk/~drg) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) Abstract: The CHemical Abstract Machine introduced by Berry and Boudol at POPL'90 is based on the chemical metaphor of floating, interacting particles and has been used to give semantics for process calculi. I will present a CHAM semantics for the (asynchronous) pi calculus due to Boudol (1992) as it strikes a nice balance between expressiveness and simplicity. -------------------------------- Date and time: Thursday 11th November 2010 at 11:00 Location: 245, School of Computer Science Title: ID-based One-Pass Authenticated Key Establishment Protocol Without Pairing Speaker: Rehana Yasmin (http://www.cs.bham.ac.uk/~rxy819/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) Abstract: Designing efficient cryptographic based security protocols for Wireless Sensor Networks (WSNs) is a challenging task due the limited resources of sensor nodes. In this talk, I will present our new efficient and secure Identity (ID) based one-pass authenticated session key establishment (ID-1P-AKE) protocol for wireless sensor networks. Our scheme does not require sensor nodes to compute any pairing function in order to compute key as compared to existing ID-based one-pass session key establishment protocols. Furthermore, a single scheme leads to a highly efficient user authentication and session key establishment scheme for WSNs. Our proposed scheme imposes very light computational and communication overhead on sensor nodes. -------------------------------- Date and time: Thursday 18th November 2010 at 11:00 Location: 245, School of Computer Science Title: Modeling and reasoning about persistent states in TPM Speaker: Shiwei Xu Abstract: There is range of agents that have persistent state, like RFID tags whose identity can be updated, databases with revocation, and TPM with Platform Configuration Register (PCR), but little work has been done in modeling persistent state with ProVerif. In this report, we take TPM with PCR as an example and model it by binary-parameter Horn Clauses. However, after being modified and tested, ProVerif still seems to have difficulty to handle this kind of situation. Furthermore, we try some other theorem provers (e.g. Prover9, Vampire), and luckily they are all able to solve the problem. Our next-step work will focus on enriching the model of TPM and continuing to consider modeling other agents which rely on persistent state. -------------------------------- Date and time: Thursday 18th November 2010 at 11:30 Location: 245, School of Computer Science Title: Authentication for Cloud Services Speaker: Ian Batten (http://www.cs.bham.ac.uk/about/people/showperson.php?person_id=5257) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) Abstract: The location of long-term keying material is a critical design decision in a distributed system. Different decisions lead to different assumptions about the properties of devices in the various roles within the system. As cloud architectures become more prevalent, accompanied by the increasing use of mobile devices, these assumptions need to be re-examined. New protocols, built on new foundations, may be needed to provide good solutions. This talk, at the outset of my research, sets out the problems I see as needing study. -------------------------------- Date and time: Thursday 16th December 2010 at 11:00 Location: 245, School of Computer Science Title: Pairing-based signed ElGamal encryption is plaintext aware Speaker: Fubiao Xia (http://www.cs.bham.ac.uk/about/people/showperson.php?person_id=4653) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) Abstract: Plaintext awareness, as a very strong security notion which accompanies semantic security can guarantee the security against chosen-cipertext attack (IND-CCA). In this talk, I will mainly give a formal proof for demonstrating the security of pairing-based signed ElGamal encryption in the random oracle model, by using some strong assumption about Schnorr signatures. Note the ordinary signed ElGamal encryption, i.e, non-pairing-based, is IND-CCA secure in the random oracle model and generic model. -------------------------------- Date and time: Thursday 13th January 2011 at 11:00 Location: 245, School of Computer Science Title: "You're nicked!": Investigating the monitoring of distributed peer-to-peer networks Speaker: Chris Novakovic (http://www.cs.bham.ac.uk/~cxn626/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) Abstract: BitTorrent, an efficient peer-to-peer file-sharing protocol, is used for distributing copyright-infringing files on the Internet. Copyright held by companies within the entertainment industries is regularly infringed; in retaliation, these industries employ the services of "copyright enforcement" companies that identify those sharing infringing files and threaten them with large fines or legal action. Previous research has shown that the technique these companies use to identify BitTorrent peers -- passive monitoring -- is inaccurate and vulnerable to subversion; more reliable techniques, such as direct peer monitoring, have been proposed but are not known to be used. In this talk, we present the results of a study we performed during August 2010, aiming to discover whether BitTorrent swarms were still being monitored, and if so, how reliably. -------------------------------- Date and time: Thursday 20th January 2011 at 11:00 Location: 245, School of Computer Science Title: Group Signatures without a trusted group manager Speaker: Chris Staite (http://www.cs.bham.ac.uk/~cxs548/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) Abstract: For the purpose of device-based identity management, each device needs to be added to a group signature. The group signature scheme has the additional requirement that devices may be revoked. Schemes currently exist which are capable of providing this, but all require a trusted group manager (in this case the identity provider). I would like to export this trust to a third party in order to provide more security to the identity. In order to do this, an extension to existing group signature schemes is shown which provides a tamper evident group signature. -------------------------------- Date and time: Thursday 3rd February 2011 at 11:00 Location: 245, School of Computer Science Title: The Seven Deadly Sins of Cloud Computing Speaker: Jon Geater Institution: THALES Information Technology Security Host: Mark Ryan Abstract: I will talk about how the move to Cloud Computing changes the information security landscape and how the old trade-offs of security, convenience and cost shift when a business moves from on-premise to serviced deployment. I will discuss some approaches to address the problems, and invite discussion from the audience to find other problems or solutions. Since the talk is effectively about risk there is no black-or-white in this discussion, so I hope for some lively debate. About me: I'm an alumnus of Birmingham university and have been an information security professional (in the area of cryptography) for over a decade. I spent most of my career as a techy with nCipher and am now CTO (Enterprise) at Thales e-security. I am active in the crypto and key management industry and most recently have founded the crypto and key management working group in the Trusted Cloud Initiative, the practical wing of the Cloud Security Alliance. -------------------------------- Date and time: Thursday 24th February 2011 at 11:00 Location: 245, School of Computer Science Title: Caveat Coercitor: coercion evident elections Speaker: Mark Ryan (http://www.cs.bham.ac.uk/~mdr/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: This talk will be to present a few ideas and get feedback. This is joint work with Peter Ryan and perhaps other. -------------------------------- Date and time: Thursday 3rd March 2011 at 11:00 Location: 245, School of Computer Science Title: Briar: a secure news and discussion system Speaker: Michael Rogers Host: Tom Chothia Abstract: Governments around the world are increasingly using surveillance and censorship of the internet to control political speech. A promising new direction for resisting such control is the construction of distributed communication networks that are partly or wholly independent from the internet. This talk will introduce Briar, a delay-tolerant publish-subscribe system based on a mixture of internet and non-internet links, which is designed to allow people in authoritarian societies to share and discuss news without fear of censorship. After outlining the design I'll present some open research problems. -------------------------------- Date and time: Thursday 31st March 2011 at 11:00 Location: 245, School of Computer Science Title: Analysing some 3G mobile protocols Speaker: Loretta Ilaria Mancini Institution: School of Computer Science, University of Birmingham Abstract: The 3G communication system was introduced in 1999 with the first release of UMTS. It aims at overcoming GSM limitations and weaknesses, while maintaining full interoperability between the two systems. In particular, it offers a better support for mobile data applications and an improved security architecture. In this talk, we present the UMTS architecture and formally analyze some protocols of the mobility management layer. More specifically, we study the anonymity and unlinkability properties of the UMTS authentication and key agreement protocol, using the ProVerif tool to verify them. Furthermore, we show a linkability attack, which exploits the use of error messages and makes it possible to link executions of the protocol originated by the same user. In particular, this attack gives an adversary a way of detecting the presence of a UMTS user in an area and in general of tracing UMTS users movements across different areas. -------------------------------- Date and time: Thursday 5th May 2011 at 11:00 Location: 245, School of Computer Science Title: Programming Language Techniques for JavaScript Isolation Speaker: Sergio Maffeis (http://www.doc.ic.ac.uk/~maffeis/) Institution: Imperial College (http://www.doc.ic.ac.uk/) Host: Marco Cova Abstract: Web sites that incorporate untrusted content may use browser- or language-based methods to keep such content from maliciously altering pages, stealing sensitive information, or causing other harm. The first part of the talk will overview my work on language based techniques to enforce host isolation and inter-component isolation on web sites that combine JavaScript components from untrusted sources. Using a formal semantics of JavaScript, we proved security properties of a subset of JavaScript, comparable in expressiveness to Facebook FBJS, obtained by combining filtering, rewriting and wrapping techniques. We validated our results by comparing with existing solutions (Facebook and AdSafe), and discovering previously unknown vulnerabilities. By turning a JavaScript subset into a capability-safe language, we showed that it is also possible to isolate mashup components from each other, thus providing a proof supporting the approach underlying Google Caja. Further progress on JavaScript isolation rests on the ability to prove functional correctness of the enforcement mechanisms, and certify “system” libraries as safe to be used by untrusted code. The second part of the talk will present my ongoing work on logic-based verification for JavaScript. Using an extension of separation logics, we derive Hoare-style proof rules for a non-trivial subset of JavaScript. The trade-off between complexity and expressiveness of local reasoning for this language is illustrated by example. -------------------------------- Date and time: Thursday 12th May 2011 at 11:00 Location: 245, School of Computer Science Title: Distributed decryption with ciphertext-plaintext unlinkability Speaker: Sergiu Bursuc Institution: School of Computer Science, University of Birmingham Abstract: To have better accountability of when decryption of encrypted data is performed, many protocols split the decryption key among a number of independent parties. As long as one of these parties is honest, decryption will be performed only according to a predefined policy. In this talk, I will present another possible advantage of such key distribution. Imagine one has a bunch of ciphertexts (i.e. encrypted plaintexts) and wants to obtain the corresponding plaintexts. However, there is a crucial additional requirement: the holders of the decryption key should not be able to discover the one-to-one correspondence between plaintexts and their respective ciphertexts. I will show that this requirement is trivially not satisfied by the standard distributed decryption algorithm, considering the particular case of El-Gamal. For El-Gamal encryption, I will show a decryption algorithm that tries to achieve ciphertext-plaintext unlinkability. This is preliminary and open work, and all feedback (attacks!) is welcome. -------------------------------- Date and time: Thursday 26th May 2011 at 11:00 Location: 245, School of Computer Science Title: Authenticated Broadcast by Sensor Nodes using Online/Offline Signature Schemes: Implementation and Evaluation Speaker: Rehana Yasmin (http://www.cs.bham.ac.uk/~rxy819/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: A Message Authentication Code (MAC) is efficient to compute on resource constrained sensor nodes. However, it cannot provide a solution to all authentication problems in Wireless Sensor Networks (WSNs). In broadcast authentication scenario, where all potential receivers share a single MAC key to authenticate messages from a sender, any compromised receiver can forge messages on behalf of any sender. Furthermore, MAC does not provide source authentication in broadcast scenario. In traditional networks, the digital signatures are preferred choice for message authentication. However, they result in increased computation time on sensor nodes which does not suit real time applications. To handle this problem, we proposed a broadcast authentication scheme for WSNs using Identity-based Online/Offline signatures. Online/Offline signatures allow to compute the complex computations of the signature generation before the message to be signed is known. Once the message is known, the singer needs to perform very minor and quick computations to get the final signature. Hence, Online/Offline signatures enable a sensor node to broadcast a real time authenticated message as soon as it has some critical event to report. The purpose of this talk is to present our experimental results of implementing Online/Offline signature schemes on actual sensor nodes. -------------------------------- Date and time: Thursday 2nd June 2011 at 11:00 Location: 245, School of Computer Science Title: Surveying the Ethical Risks of New Surveillance Technology in the DETECTER Project Speaker: John Guelke (http://www.globalethics.bham.ac.uk/staff/JohnGuelke.shtml) Institution: Centre for the Study of Global Ethics, University of Birmingham (http://www.globalethics.bham.ac.uk/) Abstract: DETECTER is a three year collaborative research project funded under the European Framework Seven Securities programme. Most research funded under this programme is concerned primarily with developing new technology or applying existing technology to current security problems. Our project by contrast, led from the University of Birmingham Centre for the Study of Global Ethics, concerns the ethical and legal norms of the use of surveillance technology. The project is carrying out original research on hot topics, like counter-terrorism data mining programmes, monitoring of Internet activity and the role of technology in pre entry screening of foreign migrants. It also is making contributions to debates on how privacy should be treated in counter-terrorism policy context from the perspective of both law and ethics. Over the course of the project I have been writing three monthly reports on developments in surveillance technology. The format of these reports have evolved over time (I'm now writing the ninth out of a total of ten). My goals have been to: a) Inform the audience (including importantly the other partners in the project about what new technologies have become available. b) Inform the audience about which technologies or proposed regulations are proving controversial in different European member states. c) Provide an overview of the ethical issues raised by these developments, summarising the ethics work we have pursued more substantively in research papers written in the course of the project. On Thursday I'll talk about the ways I've tried to do this and discuss my latest report. -------------------------------- Date and time: Thursday 9th June 2011 at 11:00 Location: 245, School of Computer Science Title: Towards a formal model for the local attacker Speaker: Dan Ghica (http://www.cs.bham.ac.uk/~drg/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: The Dolev-Yao attacker is widely used in security to model network-based intruders, to evaluate the security properties of communication protocols. A similar attacker model does not exist for “local” attacks, i.e. attacks in which the intruder has a foothold inside the computer itself via so-called “malware”. Such a model must precisely describe the interaction between legitimate code and an environment (operating system, libraries, data, etc.) which is potentially compromised. In this talk I will sketch out a recently developed theoretical framework (“system-level games”) based on operational semantics and game semantics that can describe such interactions. I will then briefly discuss under what assumptions such a framework can give rise to an interesting yet realistic attacker model. This is preliminary work and I am looking forward to your feedback. -------------------------------- Date and time: Thursday 16th June 2011 at 11:00 Location: 245, School of Computer Science Title: Peering Through the iFrame Speaker: Marco Cova (http://www.cs.bham.ac.uk/~covam/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: Drive-by-download attacks have become the method of choice for cyber-criminals to infect machines with malware. In a drive-by-download exploit, an attacker embeds a malicious script (typically written in JavaScript) into a web page. When a victim visits this page, the script is executed and attempts to compromise the browser or one of its plugins. In this talk, we examine in depth one drive-by-download campaign, that is, the coordinated efforts used to spread malware. In particular, we focus on the Mebroot campaign, which we periodically monitored and infiltrated over several months, by hijacking parts of its infrastructure and obtaining network traces at an exploit server. By studying the Mebroot drive-by-download campaign from the inside, we could obtain an in-depth and comprehensive view into the entire life-cycle of this campaign and the involved parties. More precisely, we could study the security posture of the victims of drive-by attacks(e.g., by measuring the prevalence of vulnerable software components and the effectiveness of software updating mechanisms), the characteristics of legitimate web sites infected during the campaign(e.g., the infection duration), and the modus operandi of the miscreants controlling the campaign. -------------------------------- Date and time: Thursday 7th July 2011 at 11:00 Location: 245, School of Computer Science Title: Using existing security infrastructures Speaker: Chris Mitchell (http://www.isg.rhul.ac.uk/cjm/) Institution: Royal Holloway, University of London (http://www.isg.rhul.ac.uk/) Abstract: Almost any large scale network security system requires the establishment of a security infrastructure of some kind. For example, if network authentication or authenticated key establishment is to be implemented, then the communicating parties need access to a shared secret key or certificates for each other's public keys. Setting up a new security infrastructure for a significant number of clients is by no means a trivial task. It is therefore tempting to try to exploit an existing security infrastructure to avoid the need for the potentially costly roll-out of a new infrastructure. The GAA architecture has been designed to enable the pre-existing mobile telephony security infrastructure to be exploited for the provision of generic security services. We propose the adoption of the architecture used by GAA to enable a wide range of other pre-existing infrastructures to be similarly exploited. We briefly look at two examples, namely what we refer to as TC-GAA and EMV-GAA. -------------------------------- Date and time: Thursday 4th August 2011 at 11:00 Location: 245, School of Computer Science Title: The JavaSPI Framework for Security Protocol Implementation Speaker: Alfredo Pironti (http://alfredo.pironti.eu/research/) Institution: Microsoft Research - INRIA Joint Centre (http://www.msr-inria.inria.fr/) Abstract: Many existing model-driven approaches for security protocols implementation are not widely deployed either because the starting domain-specific language is too "exotic" for the average programmer (e.g. CSP, Applied Pi Calculus), or because the graphical notation (UML security-aware profiles) is considered overkilling for the simple architecture of a security protocol. Here we present JavaSPI, a "model-driven" development framework for security protocols, whose main novelty is that the starting formal model of the protocol is itself an executable Java program, which can be developed within any familiar IDE (e.g. Eclipse, NetBeans). This Java model can then be: 1) translated into ProVerif for formal verification; 2) executed symbolically into a standard Java debugger to simulate the protocol; 3) further refined to obtain the final implementation. The development of client and server sides of the SSL handshake protocol with JavaSPI is a first step towards validation of the approach. Finally, by exploiting other frameworks like Spi2Java and its GUI, we briefly explore future research topics on "multi-view" protocol design and implementation. -------------------------------- Date and time: Thursday 22nd September 2011 at 11:00 Location: 245, School of Computer Science Title: Trivitas : Voters directly verifying votes Speaker: Gurchetan Singh (http://www.cs.bham.ac.uk/~gxs975/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: Individual verifiability is the ability of an electronic voting system to convince a voter that his vote has been correctly counted in the tally. Unfortunately, in most electronic voting systems the proofs for individual verifiability are non-intuitive and, moreover, need trusted devices to be checked. Based on the remote voting system JCJ/Civitas, we propose Trivitas, a protocol that achieves direct and end-to-end individual verifiability, while at the same time preserving coercion-resistance. Our technical contributions rely on two main ideas, both related to the notion of credentials already present in JCJ/Civitas. Firstly, we propose the use of trial credentials, as a way to track and audit the handling of a ballot from one end of the election system to the other end. We show how trial credentials can be included in JCJ/Civitas, without increased complexity on the voter end. Secondly, due to indistinguishability of credentials from random values, we observe that the association between any credential and its corresponding vote can be made public at the end of the election process, without compromising coercion-resistance. This allows voters to verify that the election system has correctly processed (encrypted, mixed and decrypted) all of their cast ballots. In particular, the voter has more intuitive and direct evidence that her intended vote has not been changed and will be counted in the final tally. -------------------------------- Date and time: Thursday 20th October 2011 at 11:00 Location: 245, School of Computer Science Title: A knowledge-based verification method for dynamic access control policies Speaker: Masoud Koleini (http://www.cs.bham.ac.uk/~mxk815/) Institution: School of Computer Science, University of Birmingham (www.cs.bham.ac.uk) Abstract: We present a new approach for automated knowledge-based verification of access control policies. The verification method not only discovers if a vulnerability exists, but also produces the strategies that can be used by the attacker to exploit the vulnerability. It investigates the information needed by the attacker to achieve the goal and whether he acquires that information when he proceeds through the strategy or not. We provide a policy language for specifying access control rules and the corresponding query language that is suited for expressing the properties we aim to verify. The policy language is expressive enough to handle integrity constraints and policy invariants. Finally, we compare the results and enhancements of the current method - implemented as a policy verification tool called PoliVer - over similar works in the context of dynamic access control policy verification. -------------------------------- Date and time: Thursday 10th November 2011 at 11:00 Location: 245, School of Computer Science Title: Modelling and reasoning about states in Late Launch based on Horn clauses Speaker: Shiwei Xu Institution: School of Computer Science, University of Birmingham Abstract: Based on the previous work on modelling systems with states, we move on in the same research area. Generally speaking, by using Horn clauses, we have modelled and verified the secrecy properties in Flicker, which is a famous trusted computing architecture making use of "Late Launch" and is quoted more than 100 times within 3 years. Compared to the previous work on modelling systems with states in Horn clauses, the main contribution of our work is that we allow one defender's code and any attacker's code (rather than one specified attacker's code) to be executed. In that way, our secret assumption is much weaker than the assumption in the previous work. The talk is divided into three parts. In the first part, Ian will briefly introduce Flicker to let us get familiar with it. In the second part, I will present a small naive example to show some basic elements, which we consider when we are modelling systems with states. In the third part, I will explain how we model Flicker, and how we allow any attacker's code to be executed. -------------------------------- Date and time: Thursday 17th November 2011 at 11:00 Location: 245, School of Computer Science Title: A game-based logical approach to reason about information-flow properties Speaker: Jérémy Dubreil (http://www.lix.polytechnique.fr/~dubreil/) Institution: Laboratoire d'Informatique de l'Ecole Polytechnique (LIX) (www.lix.polytechnique.fr) Abstract: The concept of opacity formalises the inability for an attacker, having a complete knowledge of the system structure but only partially observing its runs, to deduce secret information from the observed traces. This notion has been introduced with the objective of both simplifying and generalising several other information-flow properties. Indeed, concepts like anonymity, non-interference or non-deducibility can easily be seen as particular cases of opacity. Going further, it turns out that opacity violation corresponds the knowledge operator of epistemic logic. Using this idea, we will present in this talk a game-based logical framework using temporal and epistemic logic for reasoning in a general setting about the dynamic and conditional aspects of information disclosure. We present here a logic called SEL, for Strategic Epistemic Logic which is an extends the game-based logic ATL with epistemic modalities. We present the motivations for considering such a logic with a sequence of problems related to the verifications and enforcement of opacity properties. This will also give us the kind of games that can be used to interpret this logic. -------------------------------- Date and time: Thursday 24th November 2011 at 11:00 Location: 245, School of Computer Science Title: Presentation of the paper "A calculus for cryptographic protocols : The spi calculus", by Martin Abadi and Andy Gordon Speaker: Sergiu Bursuc Institution: School of Computer Science, University of Birmingham Abstract: Pi-calculus is a formal language designed to specify processes and reason about their properties. Can security protocols and their properties be captured in this setting? We will see that yes, they can, but at the same time we will see reasons why we have to go further than that and extend the pi-calculus. This leads to spi-calculus, where cryptographic primitives such as encryption and decryption are explicitly part of the syntax. We will consider examples of protocols in spi-calculus and show how security properties like secrecy and authenticity are expressed in this setting, and how the formal model helps in finding non-trivial attacks on these protocols. -------------------------------- Date and time: Thursday 1st December 2011 at 11:00 Location: 245, School of Computer Science Title: An encrypted general purpose processor Speaker: Peter T. Breuer (http://www.cs.bham.ac.uk/~ptb/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: I'm told the patent will be filed sometime this week or next, so perhaps I can't yet say anything about it in plaintext here! Nevertheless, I'll do my best during the actual seminar, possibly with NDA in hand. As far as the patent goes, it seems to claim "a thing with a hole in it where another thing goes" (my translation of the legalese). At any rate, the claims are certainly rather generic. That's because what it is is a computer, or a method for designing a computer (I must hack out this legalistic contamination from my skull) that works on encrypted data, yet does no encryption or decryption itself. In principle, that trick provides a secure mechanism of executing your code remotely, without giving away what the data or the code really means. After all, the encryption/decryption mechanism isn't there to be looked at or tampered with. Remarkably, all that remains as true (as it may or may not be) even if the processor is merely being run in emulation on a plain old computer (PoC). I certainly hope I'll be able to get as far as revealing some of the potential security weaknesses, and look forward to receiving your own criticisms and advice. -------------------------------- Date and time: Thursday 8th December 2011 at 11:00 Location: 245, School of Computer Science Title: Keeping Track of your Friends and Enemies: New Privacy Threats of Cellular Telecommunication Systems Speaker: Loretta Mancini (http://www.cs.bham.ac.uk/~lxm619/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: The 3GPP industry consortium has defined protocols known as UMTS which attempt to provide privacy for mobile phone users against third-party adversaries that can intercept and modify messages sent over-the-air. Those protocols are now in use by billions of subscribers. In this paper, we recall a known privacy weakness of UMTS, and we present two novel privacy attacks: one on the paging procedure and one on the UMTS Authentication and Key Agreement protocol. We show that these attacks make it possible for third parties to trace mobile phone subscribers at low cost, potentially leading to a range of serious crimes such as stalking and harassment. We demonstrate the feasibility of mounting the attacks with an implementation using a rogue femtocell. We propose protocol revisions to avoid the identified attacks. Finally, we formally analyse the privacy properties of the proposed solutions using the ProVerif tool and successfully prove that our solutions preserve users privacy. -------------------------------- Date and time: Thursday 16th February 2012 at 11:00 Location: 245, School of Computer Science Title: Can you hear the botnet? Speaker: Shishir Nagaraja (http://www.hatswitch.org/~sn275/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk) Abstract: We propose a geometrically motivated technique for isolating malicious flows in network traffic data. Our technique is particularly usable since our algorithm provides a means of representing traffic data as an audio signal. A network operator listening to the signal can track malicious flows from networked computers over time. -------------------------------- Date and time: Thursday 23rd February 2012 at 11:00 Location: 245, School of Computer Science Title: Verification of an electronic voting system with ProVerif Speaker: Sergiu Bursuc Institution: School of Computer Science, University of Birmingham Abstract: I will start with an overview of Pret a Voter - an electronic voting system designed to ensure vote privacy and integrity even in presence of a compromised voting machine. We will see how a formal model of Pret a Voter can be expressed in a process calculus that can be given as input to ProVerif. Then, vote integrity can be expressed as a correspondence property and vote privacy can be expressed as a trace equivalence property in this calculus. Both of them can be automatically verified with ProVerif, but we will see a few techniques that are required to make it work. -------------------------------- Date and time: Thursday 22nd March 2012 at 11:00 Location: 245, School of Computer Science Title: An Execution Infrastructure for TCB Minimization Speaker: Steve Dodier-Lazaro Institution: Inria Rennes Host: Mark Ryan Abstract: I will present the paper An Execution Infrastructure for TCB Minimization, from Jonathan M. McCune, Bryan Parno, Adrian Perrig, Michael K. Reiter, and Hiroshi Isozaki (accessible at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.154.453) -------------------------------- Date and time: Thursday 10th May 2012 at 11:00 Location: 245, School of Computer Science Title: TBA Speaker: Sergiu Bursuc -------------------------------- Date and time: Thursday 31st May 2012 at 11:00 Location: 245, School of Computer Science Title: Verification of security protocols with lists: from length one to unbounded length Speaker: Miriam Paiola (http://www.di.ens.fr/~paiola/) Institution: Computer Science Department, ENS Paris (http://www.di.ens.fr) Abstract: We present a novel technique for proving secrecy properties for security protocols that manipulate lists of unbounded length, for an unbounded number of sessions. More specifically, our technique relies on the Horn clause approach used in the automatic verifier ProVerif: we show that if a protocol is proven secure by our technique with lists of length one, then it is secure for lists of unbounded length. Interestingly, this theorem relies on approximations made by our verification technique: in general, secrecy for lists of length one does not imply secrecy for lists of unbounded length. Our result can be used in particular to prove secrecy properties for group protocols with an unbounded number of participants and for some XML protocols (web services) with ProVerif. -------------------------------- Date and time: Wednesday 6th June 2012 at 11:00 Location: 245, School of Computer Science Title: Mathematical Foundations for Computer Security Speaker: Michael Clarkson (http://faculty.cs.gwu.edu/~clarkson/) Institution: Department of Computer Science, The George Washington University (http://faculty.cs.gwu.edu/) Abstract: Usually, security policies on computer systems are expressed in terms of confidentiality, integrity, and availability. But we don't really know how to formalize and verify such policies. I propose an alternative: a new mathematical framework called "hyperproperties." Every security policy can be formally expressed using hyperproperties. Hyperproperties also yield a relatively complete verification methodology for an important class of security policies. And, usually, security policies are qualitative. Engineering demands quantitative metrics, though. I propose information-flow metrics that can be used to quantify security. Study of these metrics led to new discoveries: a new kind of information-flow integrity, a new model of attacker beliefs that resolves an anomaly in previous models of information-flow confidentiality, and a new connection between information flow and database privacy. That connection revealed a new theorem about the tradeoff between privacy and utility. Biography Michael Clarkson is an assistant professor in the Department of Computer Science at The George Washington University in Washington, D.C. He received a PhD in computer science from Cornell University in 2010. Clarkson's research interests include computer security and programming languages. His work focuses on using principled techniques to define security and to construct secure systems. -------------------------------- Date and time: Thursday 28th June 2012 at 11:00 Location: 245, School of Computer Science Title: Automated verification of equivalence properties of cryptographic protocols Speaker: Steve Kremer (http://www.loria.fr/~skremer/) Institution: LORIA (http://www.loria.fr/) Abstract: Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality and resistance to offline guessing attacks, and can be conveniently modeled using process equivalences. We present a novel procedure to verify equivalence properties for bounded number of sessions. Our procedure is able to verify trace equivalence for determinate cryptographic protocols. On determinate protocols, trace equivalence coincides with observational equivalence which can therefore be automatically verified for such processes. When protocols are not determinate our procedure can be used for both under- and over-approximations of trace equivalence, which proved successful on examples. The procedure can handle a large set of cryptographic primitives, namely those which can be modeled by an optimally reducing convergent rewrite system. Although, we were unable to prove its termination, it has been implemented in a prototype tool and has been effectively tested on examples, some of which were outside the scope of existing tools, including checking anonymity of an electronic voting protocol. -------------------------------- Date and time: Thursday 26th July 2012 at 11:00 Location: 245, School of Computer Science Title: Proving More Observational Equivalences with ProVerif Speaker: Vincent Cheval (http://www.lsv.ens-cachan.fr/~cheval/) Institution: Laboratoire Spécification et Vérification (http://www.lsv.ens-cachan.fr/) Abstract: Security protocols are used today to secure communication that rely on public channels like the Internet. Thus, it is essential to obtain as much confidence as possible in their correctness. Many security properties can be written as equivalence properties. Privacy, unlinkability, and strong secrecy are typical examples of equivalence properties. To our knowledge, ProVerif is the only tool relying on formal methods that can handle equivalence properties for an unbounded number of sessions. However, the notion of equivalence used by ProVerif relies on biprocesses and is stronger than the usual trace equivalence or observational equivalence and so it yields false negatives on several cases studies. First, we propose, in this paper, an extended semantics for the calculus of ProVerif that relies on destructors with inequality tests. Second, we develop an efficient algorithm that generates from a biprocess several equivalent biprocesses on which ProVerif may yield less false attack. As an example, we consider the private authentication protocol. We show why ProVerif yields a false attack on it and how our algorithm will allow ProVerif to prove the equivalence. -------------------------------- Date and time: Monday 10th September 2012 at 11:00 Location: 245, School of Computer Science Title: Trusted computing software abstractions for mobile and cloud systems Speaker: Stefan Saroiu (http://research.microsoft.com/en-us/um/people/ssaroiu/) Institution: Microsoft research Redmond (http://research.microsoft.com/) Host: Mark Ryan Abstract: Abstract: With the proliferation of smartphones running cloud-based applications, the need for trusted computing is greater than ever. Unfortunately, trusted computing abstractions today do not extend well to the needs of cloud-based mobile applications. For example, TPMs commonly found on desktops and servers today can offer "sealed storage", an abstraction that encrypts a secret and binds it to a platform's root of trust. In contrast, in the cloud, data can flow seamlessly from one node to another in an effort to take advantage of cloud's massive scalability. This creates a fundamental tension: once in the cloud, data cannot use sealed storage because that would prevent it from migrating across nodes. As another example, e-commerce or e-health mobile applications require a high-degree of trust in the data read from a smartphone's sensors. Providing the right programming abstractions and system support for building mobile trusted applications has been an open problem. In this talk, I will propose three abstractions for building cloud-based mobile applications. I will present the design and implementation of these abstractions on both x86 and ARM platforms. I will then describe the performance overhead from using these abstraction and show that such an overhead is moderate on both x86 and ARM platforms. Finally, I will describe one novel enterprise mobile application that makes use of these abstractions. Bio: Stefan Saroiu is a researcher in the Mobility and Networking Research group at Microsoft Research (MSR) in Redmond. Stefan's research interests span mobile systems, distributed systems, and computer security. For the past year, Stefan has also worked on building support for trusted computing in the ARM firmware. This firmware is required by Windows 8 in order to offer any trusted services, such as BitLocker or virtual smart cards. Before coming to MSR in 2008, Stefan spent three years as an Assistant Professor at the University of Toronto, and four months at Amazon.com as a visiting researcher where he worked on the early designs of their new shopping card system (aka Dynamo). Stefan finished his Ph.D. at the University of Washington where he was co-advised by Steve Gribble and Hank Levy. In his spare time, he enjoys spending time with with his children who have recently started to correct his English with a Romanian accent. -------------------------------- Date and time: Thursday 20th September 2012 at 11:00 Location: 245, School of Computer Science Title: Geo-Indistinguishability: Differential Privacy for Location-Based Systems Speaker: Kostas Chatzikokolakis (http://www.lix.polytechnique.fr/~kostas) Institution: LIX, Ecole Polytechnique (http://www.lix.polytechnique.fr/) Abstract: The growing popularity of location-based systems, allowing unknown/untrusted servers to easily collect and process huge amounts of users' information regarding their location, has recently started raising serious concerns about the privacy of this kind of sensitive data. In this talk I will present geo-indistinguishability, a formal notion of privacy for location-based systems that protects the exact location of a user, while still allowing approximate information, typically needed to obtain a certain desired service, to be released. This privacy definition formalizes the intuitive notion of protecting the user's location within a radius r with a level of privacy that depends on r. I will present three equivalent characterizations of this notion, one of which corresponds to a generalized version of the well-known concept of differential privacy. Furthermore, I will present a perturbation technique for achieving geo-indistinguishability by adding (controlled) random noise to the user's location, drawn from a planar Laplace distribution. The applicability of this technique will be demonstrated through two case studies: First, I will show how to enhance applications for location-based services with privacy guarantees by implementing this technique on the client side of the application. Second, the technique will be applied to sanitize location-based sensible information collected by the US Census Bureau. -------------------------------- Date and time: Thursday 4th October 2012 at 11:00 Location: 245, School of Computer Science Title: New Privacy Issues in Mobile Telephony: Fix and Verification Speaker: Loretta Manicni & Mark Ryan Institution: School of Computer Science, University of Birmingham Abstract: Mobile telephony equipment is daily carried by billions of subscribers everywhere they go. Avoiding linkability of subscribers by third parties, andprotecting the privacy of those subscribers is one of the goals of mobile telecommunication protocols. We use formal methods to model and analyse the security properties of 3G protocols. We expose two novel threats to the user privacy in 3G telephony systems, which make it possible to trace and identify mobile telephony subscribers, and we demonstrate the feasibility of a low cost implementation of these attacks. We propose fixes to these privacy issues, which also take into account and solve other privacy attacks known from the literature. We successfully prove that our privacy-friendly fixes satisfy the desired unlinkability and anonymity properties using the automatic verification tool ProVerif. -------------------------------- Date and time: Thursday 8th November 2012 at 10:00 Location: 245, School of Computer Science Title: Voting systems for Face-to-face Meetings Speaker: Mathilde Arnaud Institution: LORIA Abstract: We study a simple voting system for face-to-face meetings. While most existing systems rely on opaque electronic devices, a scientific committee of a research institute (the CNRS Section 07) has recently proposed an alternative system. Despite its simplicity (in particular, no use of cryptography), each voter can check that the outcome of the election corresponds to the votes, without having to trust the devices. In this talk, I present three versions of this system, exhibiting potential attacks, and explain how two versions ensure both vote correctness (even if the devices are corrupted) and ballot secrecy (assuming the devices are honest). -------------------------------- Date and time: Thursday 8th November 2012 at 11:00 Location: 245, School of Computer Science Title: The Speaker: Yusuke Kawamoto Institution: School of Computer Science, University of Birmingham Abstract: We present an efficient attack against widely available cryptographic devices, including the Estonian electronic ID card, security tokens and smart cards, that employ RSA key pairs. With this attack an adversary could perform cryptographic operations (i.e., decryption or signing with those devices) without knowing the corresponding RSA private key. The attack is a padding oracle attack, where a cryptographic device (behaving as a so-called `padding oracle') leaks partial information about plaintexts: The oracle never reveals the plaintexts themselves to the adversary, but returns error messages when it fails to decrypt bit strings that are given by the adversary. We modify and improve a previously known attack on RSA encryption standard PKCS#1 v1.5, which was considered to be impractical and called the `million message attack'. Our improved attack could allow an adversary to perform RSA decryption of an unknown valid ciphertext under a 1024 bit key in a mean of 50,000 and median of 15,000 oracle calls. We show how implementation details of certain devices admit an attack that requires only 9,400 oracle calls on average (3,800 median). This is joint work with Romain Bardou, Riccardo Focardi, Lorenzo Simionato, Graham Steel and Joe-Kai Tsay. -------------------------------- Date and time: Thursday 31st January 2013 at 11:00 Location: 222, School of Computer Science Title: Threat models for Building in and Managing Security Speaker: Ali E. Abdallah Institution: Birmingham City University Abstract: Threat modeling is important for information assurance, security management and for securing software. All methodologies for securing information and software systems are founded on notions for characterizing, identifying and mitigating threats. In secure software development one is asked “what is your threat model?” and on the basis of the model, claims about security can be analyzed, validated and debated. Currently, there is no agreement as to what a threat is, what its main characteristics are and how a threat formally relates to agents, assets, systems and potential attacks. The ambiguity of what threat models should capture makes them less understood, applicable and exploitable. This talk examines the design of a number of threat models with different foci and highlights their strengths and weaknesses. It shows how carefully designed threat models would enable in depth security analysis, dynamic security management and higher security assurance. Short Bio: Ali E. Abdallah is a professor of information security at Birmingham City University. Prior to current appointment, he was a professor of information assurance at London South Bank University, a lecturer in computer science at the University of Reading and a research officer at Oxford University Computing Laboratory. He lectures in information security, information risk management, software security, distributed systems and formal methods. His research interests are closely linked to his teaching and strongly emphasise the relevant theoretical underpinnings. He leads “information security” research at BCU focusing on topics ranging from identity management, access control and privacy to securing shared information in virtual organisations and the development of high assurance secure and resilient software. -------------------------------- Date and time: Thursday 21st February 2013 at 11:00 Location: 222, School of Computer Science Title: Symbolic Universal Composability Speaker: Dominique Unruh (http://www.cs.ut.ee/~unruh/) Institution: University of Tartu (http://www.ut.ee/et) Abstract: The definition of Universal Composability (UC; Canetti, FOCS 2001) is a cryptographic security definition that is both simple and gives very strong security guarantees. In particular, it ensures that the composition of secure protocols stays secure. The idea of UC is not, however, restricted to the cryptographic (computational) setting; instead, one can see it as a refinement relation on protocols and programs that preserves security and is composable. We show how UC can be applied in a symbolic security setting. We also show a new design technique (virtual primitives). This design technique allows to circumvent, in a symbolic UC setting, various impossibility results that apply in the cryptographic setting. Finally, we discuss the problem of automated verification in this setting. -------------------------------- Date and time: Friday 22nd February 2013 at 11:00 Location: 245, School of Computer Science Title: Symbolic Universal Composability Speaker: Dominique Unruh (http://www.cs.ut.ee/~unruh/) Institution: University of Tartu (http://www.ut.ee/et) Abstract: The definition of Universal Composability (UC; Canetti, FOCS 2001) is a cryptographic security definition that is both simple and gives very strong security guarantees. In particular, it ensures that the composition of secure protocols stays secure. The idea of UC is not, however, restricted to the cryptographic (computational) setting; instead, one can see it as a refinement relation on protocols and programs that preserves security and is composable. We show how UC can be applied in a symbolic security setting. We also show a new design technique (virtual primitives). This design technique allows to circumvent, in a symbolic UC setting, various impossibility results that apply in the cryptographic setting. Finally, we discuss the problem of automated verification in this setting. -------------------------------- Date and time: Thursday 28th February 2013 at 11:00 Location: 222, School of Computer Science Title: Lengths may break privacy – or how to check for equivalences with length Speaker: Vincent Cheval (http://www.cs.bham.ac.uk/~chevavfp/) Institution: School of Computer Science, University of Birmingham (www.cs.bham.ac.uk/) Abstract: Security protocols have been successfully analysed using symbolic models, where messages are represented by terms and protocols by processes. Privacy properties like anonymity or untraceability are typically expressed as equivalence between processes. While some decision procedures have been proposed for automatically deciding process equivalence, all existing approaches abstract away the information an attacker may get when observing the length of messages. In this paper, we study process equivalence with length tests. We first show that, in the static case, almost all existing decidability results (for static equivalence) can be extended to cope with length tests. In the active case, we prove decidability of trace equivalence with length tests, for a bounded number of sessions and for standard primitives. Our result relies on a previous decidability result from Cheval et al. (without length tests). Our procedure has been implemented and we have discovered a new flaw against privacy in the biometric passport protocol. -------------------------------- Date and time: Thursday 7th March 2013 at 11:00 Location: 222, School of Computer Science Title: A generic framework for three-factor authentication Speaker: Jiangshan Yu (http://www.cs.bham.ac.uk/~jxy223/) Institution: School of Computer Science, University of Birmingham (https://www.cs.bham.ac.uk/) Abstract: With widespread use of distributed systems, there is a need to protect various services and resources from unauthorized use. One way to address this concern is remote user authentication and which is widely used in distributed systems for identifying users and servers. This talk introduces a systematic approach for authenticating clients by three factors, namely password, smart-card and biometrics. In particular, a generic framework is presented. This framework can upgrade two-factor authentication schemes to three-factor authentication schemes. The derived three-factor authentication scheme achieves higher security requirement and preserves user privacy in distributed systems. -------------------------------- Date and time: Thursday 14th March 2013 at 11:00 Location: 222, School of Computer Science Title: Stateful Applied Pi Calculus: Observational Equivalence and Labelled Bisimilarity Speaker: Liu Jia Institution: School of Computer Science, University of Birmingham Abstract: We extend the applied pi calculus with state cells, which are used to reason about protocols that store persistent information. Examples are protocols involving databases or hardware modules with internal state. We distinguish between private state cells, which are not available to the attacker, and public state cells, which arise when a private state cell is compromised by the attacker. For processes involving only private state cells we define observational equivalence and labelled bisimilarity, and show that they coincide. Our result implies Abadi-Fournet's theorem in a revised version of applied pi calculus. For processes involving public state cells, we define observational equivalence, and we prove soundness of a suitably extended notion of labelled bisimilarity. -------------------------------- Date and time: Thursday 4th April 2013 at 11:00 Location: 245, School of Computer Science Title: Malicious-but-cautious certificate authorities Speaker: Mark Ryan (http://www.cs.bham.ac.uk/~mdr/) Institution: University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: Recent attacks on the key-certification mechanism has led to several proposals to improve the way certificate authorities work. In this talk, I develop some ideas around certificate transparency, and describe how a secure messaging system without trusted parties might work. -------------------------------- Date and time: Thursday 18th April 2013 at 11:00 Location: 245, School of Computer Science Title: Balancing societal security and individual privacy Speaker: Mark Ryan (http://www.cs.bham.ac.uk/~mdr/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: Mobile phones, wireless transport ticket systems, bank cards, email and web are systems which minute by minute log the minutiae of our daily lives. Although these logs are undesirable from a privacy point of view, governments and law enforcement officers like them because they are used to solve crimes. For example, about 440,000 requests by the police, local authorities and other permitted organisations to monitor telephone calls, emails and text messages were requested in a 15 month period in 2005-06 in the UK. I want to discuss some early thoughts on how the requirements of individual privacy and societal security could be balanced, and what sort of technology could make that verifiable for the citizen. It will be a short talk, because I'm mostly looking for feedback on preliminary ideas. -------------------------------- Date and time: Thursday 25th April 2013 at 11:00 Location: 245, School of Computer Science Title: On the (in)security of widely-used contactless smart cards Speaker: Flavio Garcia (http://www.cs.ru.nl/~flaviog/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: Over the last few years much attention has been paid to the (in)security of the cryptographic mechanisms used in contactless smart cards. Experience has shown that the secrecy of proprietary ciphers does not contribute to their cryptographic strength. Most notably the Mifare Classic, which has widespread application in public transport ticketing and access control systems, has been thoroughly broken in the last few years. Other prominent examples include KeeLoq and Hitag2 used in car keys and CryptoRF used in access control and payment systems. This talk briefly summarizes our own contribution to this field. We will briefly show some of the weaknesses we found in the Mifare classic. Then we will show that the security of its higher-end competitors like Atmel's CryptoRF and HID's iClass--which were proposed as a secure successor of the Mifare Classic--is not (significantly) higher. -------------------------------- Date and time: Thursday 9th May 2013 at 11:00 Location: 245, School of Computer Science Title: Static Analysis for Regular Expression Denial-of-Service Attacks Speaker: Asiri Rathnayake (http://www.cs.bham.ac.uk/~apr015/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: Regular expressions are a concise yet expressive language for expressing patterns. For instance, in networked software, they are used for input validation and intrusion detection. Yet some widely deployed regular expression matchers based on backtracking are themselves vulnerable to denial-of-service attacks, since their runtime can be exponential for certain input strings. This paper presents a static analysis for detecting such vulnerable regular expressions. The running time of the analysis compares favourably with tools based on fuzzing, that is, randomly generating inputs and measuring how long matching them takes. Unlike fuzzers, the analysis pinpoints the source of the vulnerability and generates possible malicious inputs for programmers to use in security testing. Moreover, the analysis has a firm theoretical foundation in abstract machines. Testing the analysis on two large repositories of regular expressions shows that the analysis is able to find significant numbers of vulnerable regular expressions in a matter of seconds. For more information, please refer: http://www.cs.bham.ac.uk/~hxt/research/rxxr.shtml -------------------------------- Date and time: Friday 10th May 2013 at 11:00 Location: 217, School of Computer Science Title: Caveat Coercitor: coercion-evidence in electronic voting Speaker: Gurchetan Singh and Mark Ryan (http://gurchetan.com/) Institution: School of Computer Science, University of Birmingham (http://www.cs.bham.ac.uk/) Abstract: The balance between coercion-resistance, election verifiability and usability remains unresolved in remote electronic voting despite significant research over the last few years. We propose a change of perspective, replacing the requirement of coercion-resistance with a new requirement of coercionevidence: there should be public evidence of the amount of coercion that has taken place during a particular execution of the voting system. We provide a formal definition of coercion-evidence that has two parts. Firstly, there should be a coercion-evidence test that can be performed against the bulletin board to accurately determine the degree of coercion that has taken place in any given run. Secondly, we require coercer independence, that is the ability of the voter to follow the protocol without being detected by the coercer. To show how coercion-evidence can be achieved, we propose a new remote voting scheme, Caveat Coercitor, and we prove that it satisfies coercion-evidence. Moreover, Caveat Coercitor makes weaker trust assumptions than other remote voting systems, such as JCJ/Civitas and Helios, and has better usability properties.