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.
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.
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!
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
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.
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
interactive theorem proving
automatic program synthesis