Ben Smyth: Formal verification of cryptographic protocols with automated reasoning
Name: Ben Smyth
Topic: Formal verification of cryptographic protocols with automated reasoning
Category: cryptographic protocols
Cryptographic protocols form the backbone of our digital society. Unfortunately, the security of numerous critical components has been neglected. As a consequence, attacks have resulted in financial loss, violations of personal privacy, and threats to democracy. This thesis aids the secure design of cryptographic protocols and facilitates the evaluation of existing schemes.\r\n\r\n
Developing a secure cryptographic protocol is game-like in nature, and a good designer will consider attacks against key components. Unlike games, however, an adversary is not governed by the rules and may deviate from expected behaviours. Secure cryptographic protocols are therefore notoriously difficult to define. Accordingly, cryptographic protocols must be scrutinised by experts using procedures that can evaluate security properties.\r\n\r\n
This thesis advances verification techniques for cryptographic protocols using formal methods with an emphasis on automation. The key contributions are threefold. Firstly, a definition of election verifiability for electronic voting protocols is presented; secondly, a definition of user-controlled anonymity for Direct Anonymous Attestation is delivered; and, finally, a procedure to automatically evaluate observational equivalence is introduced.\r\n\r\n
This work enables security properties of cryptographic protocols to be studied. In particular, we evaluate security in electronic voting protocols and Direct Anonymous Attestation schemes; discovering, and fixing, a vulnerability in the RSA-based Direct Anonymous Attestation protocol. Ultimately, this thesis will help avoid the current situation whereby numerous cryptographic protocols are deployed and found to be insecure.[...]
Postdoc, Ruhr University Bochum
The Cryptography Research Group at Ruhr University Bochum, Germany, is seeking for a postdoctoral researcher in cryptography (with an initial contract for one year).
Candidates must hold a PhD in mathematics, computer science or related areas. Furthermore, they must have a demonstrated record of top-quality research in foundations of public-key cryptography. This is usually proved by publications in IACR conferences or workshops.
Please send your application per email (preferably as PDF) to Eike Kiltz (eike.kiltz at rub.de). The application should include a full CV, a cover letter motivating you application, a short description of your two best research articles, and at least two candidates for reference letters. Review of applications will begin immediately and will continue until the position is filled, the starting date is flexible.
PhD in Network Security and Computer Forensics, University of Bristol
We are looking for a PhD student to work in the areas of Network Security and Computer Forensics. The position would suit students with a strong background in networking, operating systems and programming.
Candidates must have, or expect to obtain, an excellent first degree (or equivalent) in Computer Science or Electrical & Electronic Engineering. The nature of the project will require the candidate to develop a good appreciation for legal and law enforcement aspects of IT and Internet abuse. Therefore, applicants should also have a willingness to work in an interdisciplinary environment and acquire more skills (theoretical and practical) throughout the project duration.
This 3 year studentship will cover tuition fees at the home/EU rate and a basic tax-free stipend of at least £13,590 per year.
Applications can be made online from the 3rd October at the link below
Please read the Before you apply section of this page for admissions statements, entry requirements and frequently asked questions. When you apply you will be asked to select a PhD programme by department, please select the department which best matches your research interests. Please also state the research group you are interested in working with in the Research Details section of the application form.
The online system is currently closed for essential maintenance; if you would prefer to submit a paper application before the 3rd October, please email pg-admissions (at) bristol.ac.uk for a PDF version of the form, stating the studentship to which you are applying.
Post-Doc, Computer Science and Technology Centre (CCTC) at Universidade do Minho, Braga, Portugal
The Cryptography and Information Security group at CCTC/Universidade do Minho is seeking a highly-qualified, self-motivated researcher to participate in European and national research projects.
The successful candidate will be responsible for the scientific area associated with side-channel attack resilience in the design and implementation of cryptographic protocols. The candidate should have 2 years post-doctoral experience and a solid publication record in at least one of the following areas: 1) the efficient implementation of low-level cryptographic primitives and countermeasures against side-channel attacks; 2) the theoretical aspects of side-channel attack resilience (e.g. leakage resilient cryptography).
Salary: 24K EUR per Year
Duration: 1 Year (renewable)
Four Post-Doc Positions in Security and Privacy, Universitat Rovira i Virgili
Four post-doc positions from a.s.a.p. up to December 2012 are offered at Universitat Rovira i Virgili, Tarragona, Catalonia. The university is located on the Mediterranean coast, 80 km. south from Barcelona.
These are pure research positions, without teaching duties, in the context of the ARES project (http://www.aresproject.org). Successful candidates are supposed to publish in security and privacy in a broad sense.
Depending on when the candidate got her/his Ph.D., we can offer junior or senior post-docs, an international work environment and plenty of travel money to present results at security and privacy conferences.
Post-Doc, University of Warsaw
Faculty of Mathematics, Informatics and Mechanics of the University of Warsaw is looking for a post-doctoral fellow to work on the project \\\"Cryptographic Protocols Provably-Secure Against Physical Attacks\\\". The candidate must have a PhD degree, ideally in cryptography, or in a related field.
starting date: 1.12.2011 (negotiable)
duration: 2.5 years (negotiable)
Goutam Paul: Analysis and Design of RC4 and Its Variants
Name: Goutam Paul
Topic: Analysis and Design of RC4 and Its Variants
Category: secret-key cryptography
Description: The main focus of this thesis is the analysis of RC4 stream cipher and its implications in the design issues of shuffle-exchange paradigm of stream cipher.\r\n
\r\nThe RC4 stream cipher has two components. These are the Key Scheduling Algorithm (KSA) and the Pseudo-Random Generation Algorithm (PRGA). The KSA uses a secret key $K[0\\ldots l-1]$ of $l$ bytes to scramble a permutation $S[0\\ldots N-1]$ of $N$ bytes using two indices $i$ and $j$. The PRGA uses this scrambled permutation and performs further shuffle-exchanges to produce keystream output bytes $z_1, z_2, z_3,\\ldots$.\r\n
\r\nFirst, we perform a detailed theoretical analysis of RC4 KSA. We derive explicit formulae for the probabilities with which the permutation bytes $S[y]$ at any stage of the KSA are biased to the secret key. Theoretical proofs of these probabilities have been left open since Roos\' observation (1995). Along the same line, we analyze a generalization of the RC4 KSA corresponding to a class of update functions of\r\nthe indices involved in the swaps and find that such weaknesses are intrinsic in shuffle-exchange kind of key scheduling. Moreover, for the first time we show that biases towards the secret key also exist in $S[S[y]], S[S[S[y]]]$, and so on, for initial values of $y$. We also study a weakness of the RC4 Key Scheduling Algorithm (KSA) that has already been noted by Mantin and Mironov. We present a simple proof that each permutation byte after the KSA is\r\nsignificantly biased (either positive or negative) towards many values in the range $0, \\ldots, N-1$. Further, we present a detailed empirical study over Mantin\'s work when the theoretical formulae vary significantly from\r\nexperimental results due to repetition of short keys in RC4.\r\n
\r\nBased on our analysis of the key scheduling, for the first time we show that the secret key of RC4 can be recovered from the state information in a time much less than the exhaustive search with good probability. Our research ge[...]
Ph.D. student, University of Luxembourg
We are looking for a Ph.D. student in the area of formal methods based approaches to computer security and electronic privacy. The successful candidate will join the SaToSS group led by Prof. Dr. Sjouke Mauw.
- A Master\'s degree in Computer Science, Mathematics, or a related field.
- Prior exposure to and strong interest in formal methods.
- Prior exposure to and strong interest in computer and information security.
- Inquisitiveness, creativity, critical attitude.
- Very good written and oral English skills.
The candidate will be employed as a Junior Researcher at the Faculty of Sciences, Technology and Communication of the University of Luxembourg. The initial contract will be for three years (40 hours/week) with a six month trial period. The contract may be extended once by one year.