Automatic Synthesis of ZRTP Protocol Code

People

Research areas

Description

Task: Use the Coq theorem prover to specify the ZRTP protocol in logic
and then use Coq's automated program synthesis methodology to general
code that implements this protocol.
 

Goals

To be a competent user of modern interactive theorem proving
technology.  To be familiar with the uses of communication protocols
and their uses in cyber security. To become familiar with research in
logic and computation.
 

Requirements

A good background in maths is essential. Some
familiarity with a functional programming language such as Haskell,
ML, OCaml, or Scala will be useful, but not essential. You do not have
to be a hacker-level programmer!
 

Background Literature


VoIP
https://en.wikipedia.org/wiki/Voice_over_IP

Voice over IP (VoIP) is a methodology and group of technologies for
the delivery of voice communications and multimedia sessions over
Internet Protocol (IP) networks, such as the Internet. Other terms
commonly associated with VoIP are IP telephony, Internet telephony,
broadband telephony, and broadband phone service.

The ZRTP protocol
https://en.wikipedia.org/wiki/ZRTP

ZRTP (composed of Z and Real-time Transport Protocol) is a
cryptographic key-agreement protocol to negotiate the keys for
encryption between two end points in a Voice over Internet Protocol
(VoIP) phone telephony call based on the Real-time Transport
Protocol. It uses Diffie–Hellman key exchange and the Secure Real-time
Transport Protocol (SRTP) for encryption. ZRTP was developed by Phil
Zimmermann, with help from Bryce Wilcox-O'Hearn, Colin Plumb, Jon
Callas and Alan Johnston and was submitted to the Internet Engineering
Task Force (IETF) by Zimmermann, Callas and Johnston on March 5, 2006
and published on April 11, 2011 as RFC 6189.

Signal
https://whispersystems.org/blog/signal/
 

Gain

This project will prepare you for either further research in
logic and computation, or for a role in the burgeoning cyber security
industry. The scholarship from ASD (conditions apply) is intended to
encourage you to consider joining ASD after you graduate.

Scholarships: we are currently negotiating with the Australian Signals
Directorate (ASD) to obtain $5000 scholarships for students who
undertake this project. Conditions apply so if you are interested then
contactus.

 

Keywords

logic

formal verification

interactive theorem proving

automatic program synthesis

security protocols

cyber security

 

Updated:  15 May 2018/Responsible Officer:  Head of School/Page Contact:  CECS Marketing