Maude Specifications for "Formal Analysis of RFC 8120 Mutual Authentication Protocol for HTTP"

1. DH.maude - Specification of the the Diffie-Hellman Key Exchange Protocol;
2. map4http.maude - Specification of the RFC 8120 protocol such that the assumption that the cryptsystem used is perfect;
3. map4http-leak-cr.maude - Specification of the RFC 8120 protocol under the assumption that random numbers generated by clients are leaked to the intruder;
4. map4http-leak-sr.maude - Specification of the RFC 8120 protocol under the assumption that random numbers generated by servers are leaked to the intruder (for K-SEC, C-CORR and S-CORR);
5. map4http-leak-sr-NoMPA.maude - Specification of the RFC 8120 protocol under the assumption that random numbers generated by servers are leaked to the intruder (for NoMPA);
6. map4http-revised.maude - Specification of a revised version of the RFC 8120 protocol;
7. map4http-OTPW.maude - Specification of another revised version of the RFC 8120 protocol in which the Lamport one-time password scheme is used.

For the Diffie-Hellman Key Exchange Protocol, the two properties are model checked:
- Key Secrecy Property (K-SEC) – Whenever a non-intruder client C and a non-intruder server S believe that they have successfully exchanged one key k with each other in a session, the intruder never knows it.
- No Middle Person Attack (No-MPA) – The following situation never happens: a non-intruder client C believes that C has successfully exchanged a key k1 with a non-intruder server S in a session, S believes that S has successfully exchanged a key k2 with C in the same session, k1 is different from k2 and the intruder knows both k1 and k2.

No counterexample is found for K-SEC, while a counterexample is found for No-MPA.

For the RFC 8120 protocol, the four properties are model checked:
- Key Secrecy Property (K-SEC) – Whenever a non-intruder client C and a non-intruder server S believe that they have successfully exchanged one key k in a session, the intruder never knows it.
- No Middle Person Attack (No-MPA) – The following situation never happens: a non-intruder client C believes that C has successfully exchanged a key k1 with a non-intruder server S in a session, S believes that S has successfully exchanged a key k2 with C in the same session, k1 is different from k2 and the intruder knows both k1 and k2.
- Correspondence Property from a client point of view (C-CORR) – Whenever a non-intruder client C has sent a non-intruder server S an m1 message and the m3 message corresponding to the m1 message in a session SID, S has really sent C the m2 and m4 messages corresponding to those messages in the session SID.
- Correspondence Property from a server point of view (S-CORR) – Whenever a non-intruder server S has sent a non-intruder client C an m2 message and the m4 message corresponding to the m2 message in a session SID, C has really sent S the m1 and m3 messages corresponding to those messages in the session SID.

Under the assumption that the cryptsystem used is perfect, no counterexample is found for K-SEC and No-MPA, while counterexamples are found for C-CORR and S-CORR.

Under the assumption that random numbers generated by clients are leaked to the intruder, the results are the same.

Under the assumption that random numbers generated by servers are leaked to the intruder, counterexamples are found for K-SEC and No-MPA.

Under the assumption that random numbers generated by servers are leaked to the intruder, a revised version of the 8120 protocol is likely to enjoy the four properties.

If the Lamport one-time password scheme is adopted, then even under the assumption that one password shared by C and S happens to be leaked to the intruder when the session for which the password is used is over and randoms numbers generated by clients and servers a further revised version seems to enjoy the four properties but it is impossible to model check any of the four properties due to the state explosion problem. It is one piece of our future work to remedy the situation.