Top   in Index   Prev   Next

TR 33.902
Formal Analysis of the 3G Authentication Protocol

3GPP‑Page   ETSI‑search   ToC  
V4.0.0 (Wzip)  2001/10  10 p.
V3.1.0  1999/12  10 p.
Dr. Horn, Guenther

full Table of Contents for  TR 33.902  Word version:  4.0.0

Here   Top

1  Scopep. 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  Referencesp. 5

3  Definitions and Abbreviationsp. 5

4  Formal analysesp. 5

A  Formal Analysis of the 3G Authentication Protocol with Modified Sequence Number Managementp. 6

B  Formal analysis of 3G authentication and key agreement protocolp. 38

$  Change historyp. 47

Up   Top