TR 33.902
Formal Analysis of the 3G Authentication Protocol
V4.0.0 (Wzip)
2001/10 10 p.
V3.1.0
1999/12 10 p.
- Rapporteur:
- Dr. Horn, Guenther
full Table of Contents for TR 33.902 Word version: 4.0.0
1 Scope p. 5
This report contains formal analyses of the authentication and key agreement (AKA) protocol specified in 3G TS 33.102. These analyses are carried out using various means of formal logic suitable for demonstrating security and correctness properties of the AKA protocol.
The structure of this technical specification is as follows:
- clause 2 lists the references used in this specification;
- clause 3 lists the definitions and abbreviations used in this specification;
- clause 4 refers to the main body of this report. The main body is only referred to because it is not available in Word-, but only in pdf-format. The corresponding .pdf-documents are attached to this document.
2 References p. 5
3 Definitions and Abbreviations p. 5
4 Formal analyses p. 5
4.1 Formal analysis of the 3G authentication protocol with modified sequence number management p. 5
4.2 Formal analysis of the 3G authentication and key agreement protocol p. 5
A Formal Analysis of the 3G Authentication Protocol with Modified Sequence Number Management p. 6
B Formal analysis of 3G authentication and key agreement protocol p. 38
$ Change history p. 47
