Formal analysis of RFC 8120 authentication protocol for HTTP under different assumptions.

The authentication protocol for HTTP proposed in RFC 8120 has been model checked under different assumptions. Four security properties have been taken into account: (1) Key Secrecy Property (K-SEC), (2) Key Sharing Property (K-SHR), (3) Correspondence Property from a client point of view (C-CORR), and (4) Correspondence Property from a server point of view (S-CORR). In each assumption, we suppose that there exists an intruder that eavesdrops on the network and forges messages based on any pieces of information available. Under the assumption (a) that the cryptosystem used is perfect, the formal analysis concludes that the protocol is likely to enjoy K-SEC and K-SHR, but reveals that it enjoys neither C-CORR nor S-CORR. Under the assumption (b) that pseudo-random numbers generated by clients are leaked to the intruder, the results are the same. Under the assumption (c) that pseudo-random numbers generated by servers are leaked to the intruder, however, the protocol enjoys neither K-SEC nor K-SHR. To discover a realistic counterexample for K-SHR, a model checking experiment has been divided into multiple smaller ones. We then propose a revised version, which is likely to enjoy all four properties even under the assumption (c).