pq-ikev2-full-model.spthy

/*
 * Protocol:	PQ-IKEv2
 * Modeler:	Tobias Heider & Stefan-Lukas Gazdag & Sophia Grundner-Culemann
 * Date:	09/2021
 * Status:	Done
 */

theory IKEv2
begin

builtins: asymmetric-encryption, diffie-hellman, hashing, signing,
    symmetric-encryption
functions: hmac/2

/* Tells Tamarin that whenever a Eq action occurs the two arguments must be equal */
restriction Eq_check_succeed: "All x y #i. Eq(x,y) @ i ==> x = y"

// IKEv2 Protocol

/*
 * Static Longterm Key generator
 * Keys are bound to an ID i, which is not public
 */
rule generate_static:
	[ Fr(~ltk)]
	--[GenStatic(pk(~ltk))]->
	[ !PrivKey($I, ~ltk)
	, !PubKey($I, pk(~ltk))
	, Out(pk(~ltk))
	]

/*
 * Key Reveals as defined in the adversary model
 */
rule reveal_static:
	[ !PrivKey($I, ltk) ]
	--[RevLtk($I)]->
	[ Out(ltk) ]

rule reveal_dh:
	[ !DHtoReveal($I, k) ]
	--[RevDH($I)]->
	[ Out(k) ]

rule reveal_dhq:
	[ !DHQtoReveal($I, k) ]
	--[RevDHQ($I)]->
	[ Out(k) ]

/*
 * IKEv2 Protocol transitions
 */
rule IKE_SA_INIT_I:
let
	epI = 'g'^~eI	// < Initiator DH public share
	msg1 = <~spiI, 'IKE_SA_INIT', '1', 'i', epI, ~nI>
in
	[
	  Fr(~nI)	// < Initiator Nonce
	, Fr(~spiI)	// < Initiator SPI
	, Fr(~eI)	// < Initiator DH private share
	]
	--[ I0($I, ~spiI) ]->
	[
	/*
	 * HDR, SAi1, KEi, Ni  -->
	 */
	  Out(msg1)
	, StateInitI($I, ~spiI, ~eI, ~nI, msg1)
	, !DHtoReveal($I, ~eI)
	]

rule IKE_INTERMEDIATE_I:
let
	msg2 = <spiI, spiR, 'IKE_SA_INIT', '1', 'r', epR, nR>

	/*
	 * Generate First Keying Material
	 *
	 * In IKEv2 keys are read bytewise from a procedural generated byte
	 * output. In the model we have no concept of bytes, thus each key
	 * is a single block.
	 */
	k = epR^eI
	keymat = h(<nI, nR>, k)

	encr_pl_I = senc{<'g'^~peI, ~nI2>}keymat
	integ_I = hmac(<spiI, spiR, 'IKE_INTERMEDIATE', '2', 'i', encr_pl_I>, keymat)
	msgINT = <spiI, spiR, 'IKE_INTERMEDIATE', '2', 'i', encr_pl_I, integ_I>

in
	[ In(msg2)
	, Fr(~peI)
	, Fr(~nI2)
	, StateInitI($I, spiI, eI, nI, msg1)
	]
	--[ Agreed(<spiI, spiR>, $I, 'initiator', <nI, nR>, keymat)
	  , INTERMEDIATE_I($I, $R)
        ]->
	[ Out(msgINT)
	, StateIntermI($I, $R, spiI, spiR, nI, nR, ~nI2, keymat, msg1, msg2, msgINT, 'g'^eI,
	    epR, ~peI)
	, !DHQtoReveal($I, ~peI)
	]

rule IKE_AUTH_I:
let
	encr_pl_R = senc{<pepR, nR2>}keymat_old
	integ_R = hmac(<spiI, spiR, 'IKE_INTERMEDIATE', '2', 'r', encr_pl_R>, keymat_old)
	msgINT2 = <spiI, spiR, 'IKE_INTERMEDIATE', '2', 'r', encr_pl_R, integ_R>

	/*
	 * Generate Keying Material
	 *
	 * In IKEv2 keys are read bytewise from a procedural generated byte
	 * output. In the model we have no concept of bytes, thus each key
	 * is a single block.
	 */
	pq = pepR^peI
	keymat = h(keymat_old, <pq, nI2, nR2>)

	/*
	 * Authentication and validity of IKE_SA_INIT
	 */
	IntAuth_1_I = hmac(keymat, <'g'^peI, nI2, msgINT>)
	IntAuth_1_R = hmac(keymat, <pepR, nR2, msgINT2>)
	signed_octets_I = <msg1, nR, h(~idI, keymat), IntAuth_1_I, IntAuth_1_R>
	auth_pl_I = sign(signed_octets_I, skI)
	encr_pl_I = senc{<~idI, auth_pl_I, pkI>}keymat
	integ_I = hmac(<spiI, spiR, 'IKE_AUTH', '3', 'i', encr_pl_I>, keymat)
	msg3 = <spiI, spiR, 'IKE_AUTH', '3', 'i', encr_pl_I, integ_I>
in
	[ In(msgINT2)
	, StateIntermI($I, $R, spiI, spiR, nI, nR, nI2, keymat_old, msg1, msg2,
	    msgINT, epI, epR, peI)
	, Fr(~idI)
	, !PrivKey($I, skI)
	, !PubKey($I, pkI)
	]
	--[ Agreed(<spiI, spiR>, $I, 'initiator', <nI2, nR2>, keymat)
	]->
	[ Out(msg3)
	, StateAuthI($I, $R, ~idI, spiI, spiR, nI, nR, keymat_old, keymat, msg1, msg2,
	    epI, epR, 'g'^peI, pepR, IntAuth_1_I, IntAuth_1_R)
	]

rule IKE_AUTH_COMPLETE:
let
	signed_octets_R = <msg2, nI, h(idR, keymat), IntAuth_1_I, IntAuth_1_R>
	encr_pl_R = senc{<idR, spiC, auth_pl_R, pkR>}keymat
	integ_R = hmac(<spiI, spiR, 'IKE_AUTH', '3', 'r', encr_pl_R>, keymat)
	msg4 = <spiI, spiR, 'IKE_AUTH', '3', 'r', encr_pl_R, integ_R>

	/* Confirmation message (models an ESP packet encrypted with the newly
 	 * derived initial Child SA */
	ck = hmac(keymat, <nI, nR>)
	mTest = <'0', senc('test', ck),
	    hmac(<'0', senc('test',ck)>, ck)>
in
	[ In(msg4)
	, StateAuthI($I, $R, idI, spiI, spiR, nI, nR, keymat_old, keymat, msg1, msg2,
	    epI, epR, pepI, pepR, IntAuth_1_I, IntAuth_1_R)
	, !PubKey($R, pkR)
	]
	--[ Eq(verify(auth_pl_R, signed_octets_R, pkR), true)
          , IKeys($I, $R, spiC, ck)
	  , Completed(<spiI, spiR>, $I, 'initiator', $R, keymat)
          , IdentityLearnt(idR)
	  ]->
	[ Out(mTest)
	]

rule IKE_SA_INIT_R:
let
	epR = 'g'^~eR
	/*
	 * Generate Keying Material
	 *
	 * In IKEv2 keys are read bytewise from a procedural generated byte
	 * output. In the model we have no concept of bytes, thus each key
	 * is a single block.
	 */
	k = epI^~eR
	keymat = h(<nI, ~nR>, k)

	/*
	 * Messages for auth hash
	 */
	msg1 = <spiI, 'IKE_SA_INIT', '1', 'i', epI, nI>
	msg2 = <spiI, ~spiR, 'IKE_SA_INIT', '1', 'r', epR, ~nR>
in
	[ In(msg1)	// < HDR, SAi1, KEi, Ni
	, Fr(~nR)	// < Responder Nonce
	, Fr(~spiR)	// < Responder SPI
	, Fr(~eR)	// < Responder DH private share
	]
	--[ Agreed(<spiI, ~spiR>, $R, 'responder', <nI, ~nR>, keymat)
	]->
	[
	  Out(msg2)	// < HDR, SAr1, KEr, Nr
	, StateInitR($I, $R, spiI, ~spiR, nI, ~nR, keymat, msg1, msg2, epI, epR)
	, !DHtoReveal($R, ~eR)
	]

rule IKE_INTERMEDIATE_R:
let
	/* Incoming */
	encr_pl_I = senc{<pepI, nI2>}keymat_old
	integ_I = hmac(<spiI, spiR, 'IKE_INTERMEDIATE', '2', 'i', encr_pl_I>, keymat_old)
	msgINT = <spiI, spiR, 'IKE_INTERMEDIATE', '2', 'i', encr_pl_I, integ_I>

	/*
	 * Generate Updated Keying Material
	 */
	pq = pepI^~peR
	keymat = h(keymat_old, <pq, nI2, ~nR2>)

	/* Outgoing */
	encr_pl_R = senc{<'g'^~peR, ~nR2>}keymat_old
	integ_R = hmac(<spiI, spiR, 'IKE_INTERMEDIATE', '2', 'r', encr_pl_R>, keymat_old)
	msgINT2 = <spiI, spiR, 'IKE_INTERMEDIATE', '2', 'r', encr_pl_R, integ_R>
in
	[ In(msgINT)
	, Fr(~peR)
	, Fr(~nR2)
	, StateInitR($I, $R, spiI, spiR, nI, nR, keymat_old, msg1, msg2, epI, epR)
	]
	--[ Agreed(<spiI, spiR>, $R, 'responder', <nI2, ~nR2>, keymat)]->
	[ Out(msgINT2)
	, StateIntermR($I, $R, spiI, spiR, nI, nR, nI2, ~nR2, keymat_old, keymat,
	    msg1, msg2, msgINT, msgINT2, epI, epR, pepI, 'g'^~peR)
	, !DHQtoReveal($R, ~peR)
	]

rule IKE_AUTH_R:
let
	/* Incoming */
	encr_pl_I = senc{<idI, auth_pl_I, pkI>}keymat
	integ_I = hmac(<spiI, spiR, 'IKE_AUTH', '3', 'i', encr_pl_I>, keymat)
	msg3 = <spiI, spiR, 'IKE_AUTH', '3', 'i', encr_pl_I, integ_I>

	IntAuth_1_I = hmac(keymat, <pepI, nI2, msgINT>)
	IntAuth_1_R = hmac(keymat, <pepR, nR2, msgINT2>)
	signed_octets_R = <msg2, nI, h(~idR, keymat), IntAuth_1_I, IntAuth_1_R>
	auth_pl_R = sign(signed_octets_R, skR)
	encr_pl_R = senc{<~idR, ~spiC, auth_pl_R, pkR>}keymat
	integ_R = hmac(<spiI, spiR, 'IKE_AUTH', '3', 'r', encr_pl_R>, keymat)
	msg4 = <spiI, spiR, 'IKE_AUTH', '3', 'r', encr_pl_R, integ_R>

	signed_octets_I = <msg1, nR, h(idI, keymat), IntAuth_1_I, IntAuth_1_R>
in
	[ In(msg3)
	, StateIntermR($I, $R, spiI, spiR, nI, nR, nI2, nR2, keymat_old, keymat,
	    msg1, msg2, msgINT, msgINT2, epI, epR, pepI, pepR)
	, Fr(~idR)
	, Fr(~spiC)
	, !PrivKey($R, skR)
	, !PubKey($R, pkR)
	, !PubKey($I, pkI)
	]
	--[ Eq(verify(auth_pl_I, signed_octets_I, pkI), true)
	  , AUTH_R($I, $R)
	  , Completed(<spiI, spiR>, $R, 'responder', $I, keymat)
          , IdentityLearnt(~idR)
	  ]->
	[ Out(msg4)
	, ChildSAR($I, $R, ~spiC, hmac(keymat, <nI, nR>))
	]

rule ChildSA_Confirm_R:
	[ In(<'0', senc('test', ck),
	    hmac(<'0', senc('test',ck)>, ck)>)
	, ChildSAR($I, $R, spiC, ck)
	]
	--[ RConfirm($I, $R, spiC, ck)
	]->
	[
	]

/*
 * == Session Exist Traces ===
 */

lemma exists_session: exists-trace
    "Ex I R spi ck #i #j .
        IKeys(I, R, spi, ck) @ i
        & RConfirm(I, R, spi, ck) @ j
	& i < j"

lemma exists_two_sessions: exists-trace
    "Ex I R spi spi2 ck ck2 #i #j #i2 #j2 .
        IKeys(I, R, spi, ck) @ i
        & RConfirm(I, R, spi, ck) @ j
	& i < j
        & IKeys(I, R, spi2, ck2) @ i2
        & RConfirm(I, R, spi2, ck2) @ j2
	& i2 < j2
	& i < i2
	& not (ck=ck2)"

/*
 * === Authentication ===
 *
 * Initiator and Responder are able to complete the handshake and agree on a
 * common key. This follows the work in "A Hierarchy of Authentication
 * Specifications" by Lowe et al.
 */

lemma aliveness_i[use_induction]:
/* A protocol guarantees to an initiator I aliveness of another agent R if,
 * whenever I (acting as initiator) completes a run of the protocol,
 * apparently with responder R, then R has previously been running the protocol
 */
    "All spi I R keymat #i .
        Completed(spi, I, 'initiator', R, keymat) @ #i
        & not (Ex #k . RevLtk(R) @ k)
    ==> (Ex spi2 peer role keymat2 #j . Completed(spi2, R, role, peer, keymat2) @ #j
        & #j < #i)"
		
lemma aliveness_r[use_induction]:
/* A protocol guarantees to an responder R aliveness of another agent I if,
 * whenever R (acting as responder) completes a run of the protocol,
 * apparently with initiator I, then I has previously been running the protocol
 */
    "All spi I R keymat #i .
        Completed(spi, R, 'responder', I, keymat) @ #i
        & not (Ex #k . RevLtk(I) @ k)
    ==> (Ex spi2 peer role keymat2 #j . Completed(spi2, I, role, peer, keymat2) @ #j
        & #j < #i)"
		
lemma weak_agreement_i[use_induction]:
/* A protocol guarantees to an initiator I weak agreement with
 * another agent R if, whenever I (acting  as  initiator) completes a run of
 * the protocol, apparently with responder R, then R has previously been running
 * the protocol, apparently with I.
 */
    "All spi I R keymat #i .
        Completed(spi, I, 'initiator', R, keymat) @ #i
        & not (Ex #k . RevLtk(R) @ k)
        & not (Ex #k . RevDHQ(I) @ k)
        & not (Ex #k . RevDHQ(R) @ k)
    ==> (Ex spi2 role keymat2 #j . Completed(spi2, R, role, I, keymat2) @ #j
        & #j < #i)"

lemma weak_agreement_r[use_induction]:
/* A protocol guarantees to a responder R weak agreement with
 * another agent I if, whenever R (acting as responder) completes a run of
 * the protocol, apparently with initiator I, then I has previously been running
 * the protocol, apparently with R.
 */
    "All spi I R keymat #i .
        Completed(spi, R, 'responder', I, keymat) @ #i
        & not (Ex #k . RevLtk(I) @ k)
        & not (Ex #k . RevLtk(R) @ k)
        & not (Ex #k . RevDHQ(I) @ k)
        & not (Ex #k . RevDHQ(R) @ k)
    ==> (Ex spi2 role keymat2 #j . Completed(spi2, I, role, R, keymat2) @ #j
        & #j < #i)"

lemma agreement_i[use_induction]:
/* A protocol guarantees to an initiator I agreement with a responder R on a
 * set S if, whenever I (acting as initiator) completes a run
 * of the protocol, apparently with responder R, then R has previously been
 * running the protocol, apparently with I, and R was acting as responder in his
 * run, and the two agents agreed on the data values corresponding to all the
 * variables in S, and each such run of I corresponds to a unique run of R.
 */
    "All spi I R keymat #j .
        Completed(spi, I, 'initiator', R, keymat) @ #j
        & not (Ex #k . RevLtk(R) @ k)
        & not (Ex #k . RevDHQ(I) @ k)
        & not (Ex #k . RevDHQ(R) @ k)
    ==> (Ex spi2 #k .
        Completed(spi2, R, 'responder', I, keymat) @ #k)"
		
lemma agreement_r[use_induction]:
/* A protocol guarantees to a responder R agreement with an initiator I on a
 * set S if, whenever R (acting as responder) completes a run
 * of the protocol, apparently with initiator I, then I has previously been
 * running the protocol, apparently with R, and I was acting as initiator in his
 * run, and the two agents agreed on the data values corresponding to all the
 * variables in S, and each such run of R corresponds to a unique run of I.
 */
    "All spi I R keymat #j .
        Completed(spi, R, 'responder', I, keymat) @ #j
        & not (Ex #k . RevLtk(I) @ k)
		& not (Ex #k . RevLtk(R) @ k)
        & not (Ex #k . RevDHQ(I) @ k)
        & not (Ex #k . RevDHQ(R) @ k)
    ==> (Ex spi2 #k .
        Completed(spi2, I, 'responder', R, keymat) @ #k)"
lemma session_uniqueness:
    "All I R spi spi2 keymat role #i #j .
        Completed(spi, I, role, R, keymat) @ #i
        & Completed(spi2, I, role, R, keymat) @ #j
    ==> (#i = #j)"

/*
 * === Consistency ===
 */

lemma consistency:
    "All spi I R keymat keymat2 #i #j .
        Completed(spi, I, 'initiator', R, keymat) @ #i
        & Completed(spi, R, 'responder', I, keymat2) @ #j
        & not (Ex #k . RevLtk(R) @ k)
    ==> (keymat=keymat2)"

/*
 * === Secrecy ===
 */
lemma key_secrecy[reuse]:
    "All spi I R role keymat #i .
        Completed(spi, I, role, R, keymat) @ #i
        & not (Ex #j . RevLtk(R) @ #j)
        & not (Ex #j . RevDHQ(I) @ #j)
        & not (Ex #j . RevDHQ(R) @ #j)
    ==> not (Ex #j . K(keymat) @ #j)"

/*
 * === Identity Hiding ===
 */
lemma identity_hiding_R:
    "All spi R I keymat id #i .
        Completed(spi, R, 'responder', I, keymat) @ #i
        & IdentityLearnt(id) @ #i
        & not (Ex #k . RevLtk(I) @ #k)
        & not (Ex #k . RevDHQ(I) @ #k)
        & not (Ex #k . RevDHQ(R) @ #k)
    ==> not (Ex #j .  K(id) @ #j)"

end

// lemma identity_hiding_I:
//     "All spi I R ck id #i .
//         RConfirm(I, R, spi, ck) @ #i
//         IdentityLearnt(id) @ #i
//         & not (Ex #k . RevLtk(R) @ #k)
//         & not (Ex #k . RevDH(I) @ #k)
//         & not (Ex #k . RevDH(R) @ #k)
//     ==> not (Ex #j .  K(id) @ #j)"
// 
// end

//vim: ft=spthy