Information Technology Reference
In-Depth Information
his X.509/XML AC that proves his real IP address masked with the NAT server. The
initiator can also send a certificate request and the identity of the responder that can
host multiple services. The second exchange contains also the SA2 that can serve for
the child-SA negotiation and the TS (Traffic Selector) payloads. In the last message
the responder will assert his identity in the IDr (IDentity Responder) payload, his
CERT (Certificate) payload that contain his public key, hash the 3 messages in AUTH
payload to assure an integrity protection and complete the negotiation of a child SA.
TSi and TSr are used to assure the description of traffic to be sent.
4.3 IKE Validation with Hermes
In this section, we propose a formal validation of our proposed protocol using a model
checking tool, called Hermes [33]
[36]. Hermes computes an invariant of the intruder
knowledge to check whether the defined secrets within a protocol may be revealed.
The result is obtained without any restriction on the number of parallel sessions, the
number of participants and the size of exchanged messages. The research around
Hermes has also been supported by the EVA RNTL project [35] that aims at provid-
ing a toolbox for verifying cryptographic protocols using a protocol specification
language called LEAVA [36].
Presenting EVA abstract model is out of the scope of this paper [33]; we only pro-
vide here a high level specification of our protocol in LEVA language. This specifica-
tion is then automatically translated to an intermediate representation used as an entry
point to Hermes which compiles and verifies our proposition.
We illustrate our scenarios as a negotiation between two principals A, B that repre-
sent respectively the IPSec initiator and responder. Our goal is to open an IKE v1
phase 1 negotiation with identity protection based on X.509 identity and attribute
certificates.
IKEv1_Identity_Protection_Signature
alg : asym_algo
everybody knows alg
A, B,CA,EDHCP: principal
basetype key
keypair^alg SK, PK (principal)
SAi,SAr,Ca,Cb,Na,Nb,certreq: number
//Ks(number, number, number) : number
p, g, Xa, Xb: number // valeur publique DH éphémère
Ks: key // clé dérivée des valeurs DH et des autres
paramètres.
alias certB = { CA, B, PK(B) }_SK(CA)^alg
alias certA = { CA, A, PK(A) }_SK(CA)^alg
alias Attcert = { A, EDHCP }_SK(EDHCP)^alg
// Inital Knowledge
everybody knows alg
A knows A, SK(A), PK(A), PK(CA), certA, Ks,
EDHCP,PK(EDHCP),Attcert
B knows B, CA, SK(B), PK(B), PK(CA),certB,
Ks,EDHCP,PK(EDHCP)
//Message Knowledge
