diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..b25c15b --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +*~ diff --git a/CHANGELOG b/CHANGELOG new file mode 100644 index 0000000..5f63d74 --- /dev/null +++ b/CHANGELOG @@ -0,0 +1,3 @@ + +* added proverif proofs, both test and final ones + diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 0000000..94b1f87 --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,11 @@ + +# Contributing + +We use proverif as our main tool for formal verification. + +This is not about code verification, but about the theory behind the protocol. + +Please feel free to point out bugs (use the bug tracker), or add new proofs. + + + diff --git a/LICENSE.txt b/LICENSE.txt new file mode 100644 index 0000000..0c7a277 --- /dev/null +++ b/LICENSE.txt @@ -0,0 +1,24 @@ +Copyright (c) 2015-2016, Luca Fulchir +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + * Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + * Neither the name of the nor the + names of its contributors may be used to endorse or promote products + derived from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND +ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY +DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES +(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND +ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md index 121880b..27d030c 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,5 @@ This repository houses all theory proofs to test the Fenrir project. +NOTE: some of the proofs might be tests, of for older versions of Fenrir diff --git a/proverif/Federation.pv b/proverif/Federation.pv new file mode 100644 index 0000000..0967139 --- /dev/null +++ b/proverif/Federation.pv @@ -0,0 +1,379 @@ + +(* + * Formal definition to verify the Fenrir protocol. + * to be used with ProVerif + * + * This is to verify the correctness of the full 3-RTT handshake. + * DNSSEC is NOT verified, as it is assumed to be correct. + * + * The test *WILL* take a while... proverif says it has inserted more than 18k rules, and has a rule base of almost 12k rules. + * just leave it to work... + *) + +(* + * ============== + * Type definition + * ============== + *) + + +type host. +type sKey. (* symmetric key *) +type pubKey. (* public key for asymmetric key encryption *) +type privKey. (* private key for asymmetric key encryption *) +type nonce. (* just a nonce *) + +const leak: channel. (* to leak private material *) +const cf_full: channel. (* client-fenrir, full-security handshake *) +const cf_state: channel. (* client-fenrir, stateful handshake *) +const cf_dir: channel. (* client-fenrir, directory-synchronized handshake *) +const cs: channel. (* client-service *) +const sf: channel [private]. (* service-fenrir: since it is managed as the client-fenrir channel, this is not checked *) + +(* various stuff that should remain private *) +const Auth: nonce [private]. +const prS: privKey [private]. (* service private key *) +const prF: privKey [private]. +const prF_dir: privKey [private]. +const OTP: sKey [private]. +free csKey: sKey [private]. + + +free Rekey: bitstring. (* rekey message *) +type algorithm. +const alg_bad: algorithm. (* broken key exchange algorithm *) +const alg_good: algorithm. (* good key exchange algorithm *) +const alg_both: algorithm. (* both good and bad algorithms support*) + +(* + * ============== + * Function definition + * ============== + *) + +(* any to bitstring conversion *) +fun fromKey(sKey) : bitstring. +reduc forall a : sKey; toKey(fromKey(a)) = a. + + +(* symmetric key encription *) +fun sEnc(bitstring, sKey): bitstring. (* encrypt with symmetric key *) +reduc forall c: bitstring, k: sKey; sDec(sEnc(c,k),k) = c. (* decrypt with symmetric key *) + +(* public key definition *) +fun genPub(privKey): pubKey. (* public keys are generated from private ones *) +(* public key signing *) +fun sign(bitstring, privKey): bitstring. +reduc forall c: bitstring, k: privKey; ver(c, sign(c, k), genPub(k)) = true. (* verify signature *) + +(* some key exchange based on public keys *) +fun exchange(privKey, pubKey) : sKey. +equation forall p1 : privKey, p2 : privKey; exchange(p1, genPub(p2)) = exchange(p2, genPub(p1)). + +(* hash used by OTP, sKey based *) +fun hash(sKey) : sKey. + +(* xor function *) +fun xor(sKey, sKey) : sKey. +reduc forall a : sKey, b : sKey; unxor(xor(a, b), b) = a. +reduc forall a : sKey, b : sKey; unxor2(xor(a, b), a) = b. (* created for proverif, not used for simplicity *) + + +(* + * ============== + * Events -- used for correlation + * ============== + *) +event downgrade(). +event acceptedFenrir(sKey). +event clientConnect(sKey, sKey). +event serviceConnect(sKey). + + + +(* NOTE: in multiple places we have an if-else branch over a nonce. + * and the else branch start with an "if" that is the opposite of the first "if". + * This "if" after the else seems unnecessary but actually hugely speeds up proverif. + * reason: proverif does not have to check for all the possible nonces, as it seems + * it doesn't notice that the nonce can have only few vales, as it actually is an enum *) + +(* + * ========================================================================== + * Client definition, Full-security handshake with good and broken algorithms + * ========================================================================== + *) + +let client_full(pubF: pubKey, Auth: nonce, supported: algorithm, OTP: sKey) = + new cn1: nonce; (* Client Nonce 1 *) + new prC: privKey; (* ephemeral public key. *) + + (* Note: this nonce is technically useless, but prevents amplification/DoS attack + * also: the nonce should include a timer, but proverif doesn't check for DoS, + * and doesn't play nicely with timers, so we don't really care... + *) +(* start cookie exchange *) + out (cf_full, (cn1, supported)); + in (cf_full, (sn1: nonce, selected: algorithm, s1: bitstring, s2: bitstring)); + if ver((sn1, cn1, supported, selected), s1, pubF) = true then + if ver((sn1, selected), s2, pubF) = true then + +(* RTT 1 completed *) + + (* start algorithm agreement *) + new cn2: nonce; + (* out: nonces and signature, supported_algorithms *) + (* bad algorithm somehow exposes authentication data *) + if selected = alg_bad && (supported = alg_both || supported = alg_bad) then + ( + event downgrade() + ) + else + ( + if selected = alg_good then + out (cf_full, (sn1, selected, s2, cn2, genPub(prC))); + (* se1: server encrypt 1: contains supported authentication algorithms + * unused here, it's the same mechanism as the "selected" one + *) + in (cf_full, (ephF: pubKey, se1: bitstring, s3: bitstring)); + if ver((ephF, se1), s3, pubF) = true then + let (cfKey) = exchange(prC, ephF) in +(* RTT 2 Completed *) + out (cf_full, (sEnc((Auth, Auth), cfKey))); + in (cf_full, (se2: bitstring)); + let (chan: channel, xorKey: bitstring) = sDec(se2, cfKey) in + +(* RTT 3 completed, can now connect to service *) + + let cs_Key = sDec(xorKey, hash(OTP)) in + event clientConnect(cfKey, toKey(cs_Key)); + out (chan, sEnc(fromKey(OTP), toKey(cs_Key))) + ). + + +(* + * =========================================================================== + * Fenrir definition, full security handshake, with good and broken algorithms + * =========================================================================== + *) + +let fenrir_full(privF: privKey, Auth: nonce, supported: algorithm) = + (* Nonce exchange *) + in (cf_full, (fin1: nonce, client_alg: algorithm)); + new s_nonce: nonce; + (* triggers "event downgrade()" in the client, no need to go further *) + (* bad only if both support bad *) + if client_alg = alg_bad && (supported = alg_bad || supported = alg_both) then + ( + out (cf_full, (s_nonce, alg_bad, sign((s_nonce, fin1, client_alg, alg_bad), privF), + sign((s_nonce, alg_bad), privF))) + ) + else + ( + if client_alg = alg_good || client_alg = alg_both then + out (cf_full, (s_nonce, alg_good, sign((s_nonce, fin1, client_alg, alg_good), privF), + sign((s_nonce, alg_good), privF))); +(* RTT 1 finished *) + in (cf_full, (=s_nonce, =alg_good, signed: bitstring, fin2: nonce, pubC: pubKey)); + if ver((s_nonce, alg_good), signed, genPub(privF)) = true then + new prF2: privKey; + let (cfKey) = exchange(prF2, pubC) in + out (cf_full, (genPub(prF2), sEnc((supported, supported), cfKey), sign((genPub(prF2), sEnc((s_nonce, s_nonce), cfKey)), privF))); +(* RTT 2 finished, now we have a state *) + in (cf_full, (ce1: bitstring)); + let (data: nonce, data2: nonce) = sDec(ce1, cfKey) in + if data = Auth && data2 = Auth then + + new user_info : nonce; + out (sf, user_info); + in (sf, key : sKey); + event acceptedFenrir(cfKey); + out (cf_full, (sEnc((cs, key), cfKey))) +(* RT3 finished *) + ). + +(* + * ================================== + * Service definition, common for all + * ================================== + *) + +let service(OTP : sKey) = + (* sf channel is secret, thus trusted. do not encrypt to reduce + * proverif running time *) + in (sf, rnd : nonce); (* user info. useless in our model *) + (* this should be cskey XOR hash(OTP), but proverif can't handle XOR. + * so we treat it as encryption, as it has the same properties in our case *) + out (sf, sEnc(fromKey(csKey), hash(OTP))); + in (cs, enc2 : bitstring); + let is_OTP : bitstring = sDec(enc2, csKey) in + if OTP = toKey(is_OTP) then + event serviceConnect(csKey). + +(* + * ====================================================================== + * Client Definition, Stateful handshake, with good and broken algorithms + * ====================================================================== + *) + +let client_state (pubF: pubKey, Auth: nonce, supported: algorithm, OTP: sKey) = + new cn1: nonce; (* Client Nonce 1 *) + new prC: privKey; (* ephemeral key *) + + (* Note: this nonce is technically useless, but prevents amplification/DoS attack + * also: the nonce should include a timer, but proverif doesn't check for DoS, + * and doesn't play nicely with timers, so we don't really care... + *) +(* start cookie exchange *) + out (cf_state, (cn1, supported)); + in (cf_state, (alg: algorithm, ephF: pubKey, s1: bitstring)); + if ver((cn1, supported, alg, ephF), s1, pubF) = true then + +(* RTT 1 completed *) + + if alg = alg_bad then + ( + if supported = alg_bad || supported = alg_both then + (* bad algorithm exposes authentication data *) + event downgrade() + ) + else + ( + if alg = alg_good then + if supported = alg_good || supported = alg_both then + + let (cfKey) = exchange(prC, ephF) in + out (cf_state, (genPub(prC), sEnc((Auth,Auth), cfKey))); + in (cf_state, enc: bitstring); + +(* RTT 2 completed, can now connect to service *) + + let (chan: channel, xorKey: bitstring) = sDec(enc, cfKey) in + let cs_Key = sDec(xorKey, hash(OTP)) in + event clientConnect(cfKey, toKey(cs_Key)); + out (chan, sEnc(fromKey(OTP), toKey(cs_Key))) + ). + +(* + * =========================================================================== + * Fenrir definition, stateful handshake, with good and broken algorithms + * =========================================================================== + *) + +let fenrir_state (privF: privKey, Auth: nonce, supported: algorithm) = + (* Nonce exchange *) + new prF2 : privKey; + new s_nonce: nonce; + in (cf_state, (fin1: nonce, client_alg: algorithm)); + if client_alg = alg_bad && (supported = alg_bad || supported = alg_both) then + ( + out(cf_state, (alg_bad, genPub(prF2), sign((fin1, client_alg, alg_bad, genPub(prF2)), privF))) + ) + else + ( + if (client_alg = alg_good || client_alg = alg_both) && (supported = alg_good || supported = alg_both) then + out(cf_state, (alg_good, genPub(prF2), sign((fin1, client_alg, alg_good, genPub(prF2)), privF))); +(* RTT 1 finished *) + in (cf_state, (pubC: pubKey, enc: bitstring)); + let (cfKey) = exchange(prF2, pubC) in + let (data: nonce, data2: nonce) = sDec(enc, cfKey) in + if data = Auth && data2 = Auth then + new user_info : nonce; + out (sf, (user_info)); + in (sf, key : sKey); + event acceptedFenrir(cfKey); + out (cf_state, sEnc((cs, key), cfKey)) +(* RTT 2 finished *) + ). + + +(* + * =========================================================================== + * Client definition, directory synchronized handshake + * =========================================================================== + *) +let client_dir (pubF: pubKey, Auth: nonce, OTP: sKey) = + new prC : privKey; + new cn : nonce; + let (cfKey) = exchange(prC, pubF) in + out (cf_dir, (genPub(prC), sEnc((Auth,cn), cfKey))); + in (cf_dir, enc: bitstring); +(* RTT 1 finished, now connect to service *) + let (=cn, chan: channel, xorKey: bitstring) = sDec(enc, cfKey) in + let cs_Key = sDec(xorKey, hash(OTP)) in + event clientConnect(cfKey, toKey(cs_Key)); + out (chan, sEnc(fromKey(OTP), toKey(cs_Key))). +(* + * =========================================================================== + * Fenrir definition, directory synchronized handshake + * =========================================================================== + *) + +let fenrir_dir (privF: privKey, Auth: nonce) = + in (cf_dir, (pubC: pubKey, enc: bitstring)); + let (cfKey) = exchange(privF, pubC) in + let (=Auth, cn: nonce) = sDec (enc, cfKey) in + + new user_info : nonce; + out (sf, user_info); + in (sf, key : sKey); + event acceptedFenrir(cfKey); + out (cf_dir, sEnc((cn, cs, key), cfKey)). + + + + + + +(* + * ============== + * Event correlation: + * ============== + +query k1 : sKey, k2 : sKey; event(serviceConnect(k2)) ==> event(clientConnect(k1, k2)) ==> event(clientConnect(k1, k2)) ==> event(acceptedFenrir(k1)). + *) + +(* + * ============== + * What should be secret? + * ============== + *) + +query event(downgrade()). +query attacker(Auth). (* client auth data. *) +query attacker(OTP). (* client-service OTP data. *) + +(* + * ============== + * Run the verification + * ============== + *) + + +process + let pbF = genPub(prF) in + let pbF_dir = genPub(prF_dir) in + ((!service(OTP)) + | (!client_full (pbF, Auth, alg_both, OTP)) | (!client_full (pbF, Auth, alg_good, OTP)) + | (!fenrir_full (prF, Auth, alg_both)) | (!fenrir_full (prF, Auth, alg_good)) + | (!client_state(pbF, Auth, alg_both, OTP)) | (!client_state(pbF, Auth, alg_good, OTP)) + | (!fenrir_state(prF, Auth, alg_both)) | (!fenrir_state(prF, Auth, alg_good)) + | (!client_dir (pbF_dir, Auth, OTP)) | (!fenrir_dir (prF, Auth)) + | phase 1; out(leak, prF) +(* PFS: leaking of the long-term secret will NOT affect previous communications *) + (* Now do everything again, WITHOUT leaking. Everything must be done again since + * we leaked the previous private key. If we didn't do everything again we could not prove + * that the interaction of the handshakes is secure. + * This is because the 1-RTT handshake does NOT have long-term secret + *) +(* + ; (!service(OTP)) + | (!client_full (pbF_dir, Auth, alg_both, OTP)) | (!client_full (pbF_dir, Auth, alg_good, OTP)) + | (!fenrir_full (prF_dir, Auth, alg_both)) | (!fenrir_full (prF_dir, Auth, alg_good)) + | (!client_state(pbF_dir, Auth, alg_both, OTP)) | (!client_state(pbF_dir, Auth, alg_good, OTP)) + | (!fenrir_state(prF_dir, Auth, alg_both)) | (!fenrir_state(prF_dir, Auth, alg_good)) + | (!client_dir (pbF_dir, Auth, OTP)) | (!fenrir_dir (prF, Auth)) +*) + ) + + + diff --git a/proverif/Fenrir.pv b/proverif/Fenrir.pv new file mode 100644 index 0000000..ae5e029 --- /dev/null +++ b/proverif/Fenrir.pv @@ -0,0 +1,455 @@ + +(* + * Formal definition to verify the Fenrir protocol. + * to be used with ProVerif + * + * This is to verify the correctness of the full 3-RTT handshake. + * DNSSEC is NOT verified, as it is assumed to be correct. + * + *) + +(* + * ============== + * Type definition + * ============== + *) + + +type host. +type sKey. (* symmetric key *) +type pubKey. (* public key for asymmetric key encryption *) +type privKey. (* private key for asymmetric key encryption *) +type nonce. (* just a nonce *) + +const leak: channel. (* to leak private material *) +const cf_full: channel. (* client-fenrir, full-security handshake *) +const cf_state: channel. (* client-fenrir, stateful handshake *) +const cf_dir: channel. (* client-fenrir, directory-synchronized handshake *) +const cs: channel. (* client-service *) +const sf: channel [private]. (* service-fenrir: since it is managed as the client-fenrir channel, this is not checked *) + +(* various stuff that should remain private *) +const Auth: nonce [private]. +const prS: privKey [private]. (* service private key *) +const prF: privKey [private]. +const prC: privKey [private]. +const prF_dir: privKey [private]. +const OTP: sKey [private]. +free csKey: sKey [private]. + + +free Rekey: bitstring. (* rekey message *) +type algorithm. +const alg_bad: algorithm. (* broken key exchange algorithm *) +const alg_good: algorithm. (* good key exchange algorithm *) +const alg_both: algorithm. (* both good and bad algorithms support*) + +(* + * ============== + * Function definition + * ============== + *) + +(* any to bitstring conversion *) +fun fromKey(sKey) : bitstring. +reduc forall a : sKey; toKey(fromKey(a)) = a. + + +(* symmetric key encription *) +fun sEnc(bitstring, sKey): bitstring. (* encrypt with symmetric key *) +reduc forall c: bitstring, k: sKey; sDec(sEnc(c,k),k) = c. (* decrypt with symmetric key *) + +(* public key definition *) +fun genPub(privKey): pubKey. (* public keys are generated from private ones *) +(* public key signing *) +fun sign(bitstring, privKey): bitstring. +reduc forall c: bitstring, k: privKey; ver(c, sign(c, k), genPub(k)) = true. (* verify signature *) + +(* some key exchange based on public keys *) +fun exchange(privKey, pubKey) : sKey. +equation forall p1 : privKey, p2 : privKey; exchange(p1, genPub(p2)) = exchange(p2, genPub(p1)). + +(* hash used by OTP, sKey based *) +fun hash(sKey) : sKey. + +(* xor function *) +fun xor(sKey, sKey) : sKey. +reduc forall a : sKey, b : sKey; unxor(xor(a, b), b) = a. +reduc forall a : sKey, b : sKey; unxor2(xor(a, b), a) = b. (* created for proverif, not used for simplicity *) + + +(* + * ============== + * Events -- used for correlation + * ============== + *) +event downgrade(). +event acceptedFenrir(sKey). +event clientConnect(sKey, sKey). +event serviceConnect(sKey). + + + +(* NOTE: in multiple places we have an if-else branch over a nonce. + * and the else branch start with an "if" that is the opposite of the first "if". + * This "if" after the else seems unnecessary but actually hugely speeds up proverif. + * reason: proverif does not have to check for all the possible nonces, as it seems + * it doesn't notice that the nonce can have only few vales, as it actually is an enum *) + +(* + * ========================================================================== + * Client definition, Full-security handshake with good and broken algorithms + * ========================================================================== + *) + +let client_full(pubF: pubKey, Auth: nonce, supported: algorithm, supported_auth: algorithm, OTP: sKey) = + new cn1: nonce; (* Client Nonce 1 *) + + (* Note: this nonce is technically useless, but prevents amplification/DoS attack + * also: the nonce should include a timer, but proverif doesn't check for DoS, + * and doesn't play nicely with timers, so we don't really care... + *) +(* start cookie exchange *) + out (cf_full, (cn1, supported)); + in (cf_full, (sn1: nonce, srv_auth : algorithm, selected: algorithm, s1: bitstring, s2: bitstring)); + if ver((sn1, cn1, supported, selected, srv_auth), s1, pubF) = true then + if ver((sn1, selected, srv_auth), s2, pubF) = true then + +(* RTT 1 completed *) + + (* start algorithm agreement *) + new cn2: nonce; + (* out: nonces and signature, supported_algorithms *) + (* bad algorithm somehow exposes authentication data *) + if selected = alg_bad && (supported = alg_both || supported = alg_bad) then + ( + event downgrade() + ) + else + ( + if selected = alg_good && (supported = alg_both || supported = alg_good) then + out (cf_full, (sn1, selected, s2, cn2, genPub(prC))); + (* s_auth: server supported 1: contains supported authentication algorithms + * unused here, it's the same mechanism as the "selected" one + *) + in (cf_full, (ephF: pubKey, s3: bitstring)); + if ver((ephF, cn2), s3, pubF) = true then + let (cfKey) = exchange(prC, ephF) in +(* RTT 2 Completed *) + if srv_auth = alg_bad && (supported_auth = alg_both || supported_auth = alg_bad) then + ( + (* authentication somehow leaks info through encryption + * are we being a bit paranoid? + *) + event downgrade() + ) + else + ( + if (srv_auth = alg_both || srv_auth = alg_good) && (supported_auth = alg_both || supported_auth = alg_good) then + out (cf_full, (sEnc((Auth, Auth), cfKey))); + in (cf_full, (se2: bitstring)); + let (chan: channel, xorKey: bitstring) = sDec(se2, cfKey) in + +(* RTT 3 completed, can now connect to service *) + + let cs_Key = sDec(xorKey, hash(OTP)) in + event clientConnect(cfKey, toKey(cs_Key)); + out (chan, sEnc(fromKey(OTP), toKey(cs_Key))) + ) + ). + + +(* + * =========================================================================== + * Fenrir definition, full security handshake, with good and broken algorithms + * =========================================================================== + *) + +let fenrir_full(privF: privKey, Auth: nonce, supported: algorithm, supported_auth: algorithm) = + (* Nonce exchange *) + in (cf_full, (fin1: nonce, client_alg: algorithm)); + new s_nonce: nonce; + (* triggers "event downgrade()" in the client, no need to go further *) + (* bad only if both support bad *) + if client_alg = alg_bad && (supported = alg_bad || supported = alg_both) then + ( + out (cf_full, (s_nonce, alg_bad, supported_auth, sign((s_nonce, fin1, client_alg, alg_bad, supported_auth), privF), + sign((s_nonce, alg_bad, supported_auth), privF))) + ) + else + ( + if client_alg = alg_good || client_alg = alg_both then + out (cf_full, (s_nonce, alg_good, supported_auth, sign((s_nonce, fin1, client_alg, supported_auth, alg_good), privF), + sign((s_nonce, alg_good, supported_auth), privF))); +(* RTT 1 finished *) + in (cf_full, (=s_nonce, =alg_good, signed: bitstring, fin2: nonce, pubC: pubKey)); + if ver((s_nonce, alg_good), signed, genPub(privF)) = true then + new prF2: privKey; + let (cfKey) = exchange(prF2, pubC) in + out (cf_full, (genPub(prF2), sign((genPub(prF2), fin2), privF))); +(* RTT 2 finished, now we have a state *) + in (cf_full, (ce1: bitstring)); + let (data: nonce, data2: nonce) = sDec(ce1, cfKey) in + if data = Auth && data2 = Auth then + + new user_info : nonce; + out (sf, user_info); + in (sf, key : sKey); + event acceptedFenrir(cfKey); + out (cf_full, (sEnc((cs, key), cfKey))) +(* RT3 finished *) + ). + +(* + * ================================== + * Service definition, common for all + * ================================== + *) + +let service(OTP : sKey) = + (* sf channel is secret, thus trusted. do not encrypt to reduce + * proverif running time *) + in (sf, rnd : nonce); (* user info. useless in our model *) + (* this should be cskey XOR hash(OTP), but proverif can't handle XOR. + * so we treat it as encryption, as it has the same properties in our case *) + out (sf, sEnc(fromKey(csKey), hash(OTP))); + in (cs, enc2 : bitstring); + let is_OTP : bitstring = sDec(enc2, csKey) in + if OTP = toKey(is_OTP) then + event serviceConnect(csKey). + +(* + * ====================================================================== + * Client Definition, Stateful handshake, with good and broken algorithms + * ====================================================================== + *) + +let client_state (pubF: pubKey, Auth: nonce, supported: algorithm, supported_auth: algorithm, OTP: sKey) = + new cn1: nonce; (* Client Nonce 1 *) + + (* Note: this nonce is technically useless, but prevents amplification/DoS attack + * also: the nonce should include a timer, but proverif doesn't check for DoS, + * and doesn't play nicely with timers, so we don't really care... + *) +(* start cookie exchange *) + out (cf_state, (cn1, supported)); + in (cf_state, (alg: algorithm, srv_auth: algorithm, ephF: pubKey, s1: bitstring)); + if ver((cn1, supported, alg, srv_auth, ephF), s1, pubF) = true then + +(* RTT 1 completed *) + + if alg = alg_bad then + ( + if supported = alg_bad || supported = alg_both then + (* bad algorithm exposes authentication data *) + event downgrade() + ) + else + ( + if alg = alg_good && (supported = alg_good || supported = alg_both) then + if srv_auth = alg_bad && (supported_auth = alg_both || supported_auth = alg_bad) then + ( + event downgrade() + ) + else + ( + if (srv_auth = alg_both || srv_auth = alg_good) && (supported_auth = alg_both || supported_auth = alg_good) then + let (cfKey) = exchange(prC, ephF) in + out (cf_state, (genPub(prC), sEnc((Auth,Auth), cfKey))); + in (cf_state, enc: bitstring); + +(* RTT 2 completed, can now connect to service *) + + let (chan: channel, xorKey: bitstring) = sDec(enc, cfKey) in + let cs_Key = sDec(xorKey, hash(OTP)) in + event clientConnect(cfKey, toKey(cs_Key)); + out (chan, sEnc(fromKey(OTP), toKey(cs_Key))) + ) + ). + +(* + * =========================================================================== + * Fenrir definition, stateful handshake, with good and broken algorithms + * =========================================================================== + *) + +let fenrir_state (privF: privKey, Auth: nonce, supported: algorithm, supported_auth: algorithm) = + (* Nonce exchange *) + new prF2 : privKey; + new s_nonce: nonce; + in (cf_state, (fin1: nonce, client_alg: algorithm)); + if client_alg = alg_bad && (supported = alg_bad || supported = alg_both) then + ( + out(cf_state, (alg_bad, supported_auth, genPub(prF2), sign((fin1, client_alg, alg_bad, supported_auth, genPub(prF2)), privF))) + ) + else + ( + if (client_alg = alg_good || client_alg = alg_both) && (supported = alg_good || supported = alg_both) then + out(cf_state, (alg_good, supported_auth, genPub(prF2), sign((fin1, client_alg, alg_good, supported_auth, genPub(prF2)), privF))); +(* RTT 1 finished *) + in (cf_state, (pubC: pubKey, enc: bitstring)); + let (cfKey) = exchange(prF2, pubC) in + let (data: nonce, data2: nonce) = sDec(enc, cfKey) in + if data = Auth && data2 = Auth then + new user_info : nonce; + out (sf, (user_info)); + in (sf, key : sKey); + event acceptedFenrir(cfKey); + out (cf_state, sEnc((cs, key), cfKey)) +(* RTT 2 finished *) + ). + + +(* + * =========================================================================== + * Client definition, directory synchronized handshake + * =========================================================================== + *) +let client_dir (pubF: pubKey, Auth: nonce, OTP: sKey) = + new cn : nonce; + let (cfKey) = exchange(prC, pubF) in + out (cf_dir, (genPub(prC), sEnc((Auth,cn), cfKey))); + in (cf_dir, enc: bitstring); +(* RTT 1 finished, now connect to service *) + let (=cn, chan: channel, xorKey: bitstring) = sDec(enc, cfKey) in + let cs_Key = sDec(xorKey, hash(OTP)) in + event clientConnect(cfKey, toKey(cs_Key)); + out (chan, sEnc(fromKey(OTP), toKey(cs_Key))). +(* + * =========================================================================== + * Fenrir definition, directory synchronized handshake + * =========================================================================== + *) + +let fenrir_dir (privF: privKey, Auth: nonce) = + in (cf_dir, (pubC: pubKey, enc: bitstring)); + let (cfKey) = exchange(privF, pubC) in + let (=Auth, cn: nonce) = sDec (enc, cfKey) in + + new user_info : nonce; + out (sf, user_info); + in (sf, key : sKey); + event acceptedFenrir(cfKey); + out (cf_dir, sEnc((cn, cs, key), cfKey)). + + + + + + +(* + * ============== + * Event correlation: + * ============== + *) + +query k1 : sKey, k2 : sKey; event(serviceConnect(k2)) ==> event(clientConnect(k1, k2)). +query k1 : sKey, k2 : sKey; event(clientConnect(k1, k2)) ==> event(acceptedFenrir(k1)). + +(* + * ============== + * What should be secret? + * ============== + *) + +query event(downgrade()). +query attacker(OTP). (* client-service OTP data. *) +query attacker(Auth). (* client auth data. *) + +(* + * ============== + * Run the verification + * ============== + *) + + +process + let pbF = genPub(prF) in + let pbF_dir = genPub(prF_dir) in + ( +(* Perfect forward secrecy test. Note that the _dir methods work with non-leaked keys, as there + * is no master key + *) +(* these tests alone needs about 26k to 46k rules in proverif + * phase 0: both parts support good algorithms. + * phase 1: client supports only bad algorithms + * phase 2: auth-server supports only bad algorithms + * phase 3: leak long term secret to test perfect forward secrecy, + *) +(* +*) + (!service(OTP)) + | (!client_full (pbF, Auth, alg_both, alg_both, OTP)) | (!client_full (pbF, Auth, alg_good, alg_both, OTP)) + | (!client_full (pbF, Auth, alg_both, alg_good, OTP)) | (!client_full (pbF, Auth, alg_good, alg_good, OTP)) + | (!fenrir_full (prF, Auth, alg_both, alg_both)) | (!fenrir_full (prF, Auth, alg_good, alg_both)) + | (!fenrir_full (prF, Auth, alg_both, alg_good)) | (!fenrir_full (prF, Auth, alg_good, alg_good)) + | (!client_state(pbF, Auth, alg_both, alg_both, OTP)) | (!client_state(pbF, Auth, alg_good, alg_both, OTP)) + | (!client_state(pbF, Auth, alg_both, alg_good, OTP)) | (!client_state(pbF, Auth, alg_good, alg_good, OTP)) + | (!fenrir_state(prF, Auth, alg_both, alg_both)) | (!fenrir_state(prF, Auth, alg_good, alg_both)) + | (!fenrir_state(prF, Auth, alg_both, alg_good)) | (!fenrir_state(prF, Auth, alg_good, alg_good)) + | phase 1; + (!service(OTP)) + | (!client_full (pbF, Auth, alg_both, alg_both, OTP)) | (!client_full (pbF, Auth, alg_bad, alg_both, OTP)) + | (!client_full (pbF, Auth, alg_both, alg_bad, OTP)) | (!client_full (pbF, Auth, alg_bad, alg_bad, OTP)) + | (!fenrir_full (prF, Auth, alg_good, alg_good)) + | (!client_state(pbF, Auth, alg_both, alg_both, OTP)) | (!client_state(pbF, Auth, alg_bad, alg_both, OTP)) + | (!client_state(pbF, Auth, alg_both, alg_bad, OTP)) | (!client_state(pbF, Auth, alg_bad, alg_bad, OTP)) + | (!fenrir_state(prF, Auth, alg_good, alg_good)) + | phase 2; + (!service(OTP)) + | (!client_full (pbF, Auth, alg_good, alg_good, OTP)) + | (!fenrir_full (prF, Auth, alg_both, alg_both)) | (!fenrir_full (prF, Auth, alg_bad, alg_both)) + | (!fenrir_full (prF, Auth, alg_both, alg_bad)) | (!fenrir_full (prF, Auth, alg_bad, alg_bad)) + | (!client_state(pbF, Auth, alg_good, alg_good, OTP)) + | (!fenrir_state(prF, Auth, alg_both, alg_both)) | (!fenrir_state(prF, Auth, alg_bad, alg_both)) + | (!fenrir_state(prF, Auth, alg_both, alg_bad)) | (!fenrir_state(prF, Auth, alg_bad, alg_bad)) + | phase 3; out(leak, prF) +(* +*) +(* PFS: leaking of the long-term secret will not affect previous communications *) + (* Now do everything again, WITHOUT leaking. Everything must be done again since + * we leaked the previous private key. If we didn't do everything again we could not prove + * that the interaction of the handshakes is secure. + * This is because the 1-RTT handshake does NOT have long-term secret, so wen can't leak its private key. + *) +(* these next tests alone needs about 37k to 55k rules in proverif + * the previous and the next tests together are way too much, as proverif seems to have a huge slow down for every new phase, + * even when empty. Therefore activate either the previous or the next tests, they are independent anyway. + * pahse 0-2: like previous phase 0-2, except we add the directory synchronized handshake + * and do NOT leak the key at the end. This way we can test the interaction + * of different handshakes with the same public key. + *) +(* + (!service(OTP)) + | (!client_full (pbF_dir, Auth, alg_both, alg_both, OTP)) | (!client_full (pbF_dir, Auth, alg_good, alg_both, OTP)) + | (!client_full (pbF_dir, Auth, alg_both, alg_good, OTP)) | (!client_full (pbF_dir, Auth, alg_good, alg_good, OTP)) + | (!fenrir_full (prF_dir, Auth, alg_both, alg_both)) | (!fenrir_full (prF_dir, Auth, alg_good, alg_both)) + | (!fenrir_full (prF_dir, Auth, alg_both, alg_good)) | (!fenrir_full (prF_dir, Auth, alg_good, alg_good)) + | (!client_state(pbF_dir, Auth, alg_both, alg_both, OTP)) | (!client_state(pbF_dir, Auth, alg_good, alg_both, OTP)) + | (!client_state(pbF_dir, Auth, alg_both, alg_good, OTP)) | (!client_state(pbF_dir, Auth, alg_good, alg_good, OTP)) + | (!fenrir_state(prF_dir, Auth, alg_both, alg_both)) | (!fenrir_state(prF_dir, Auth, alg_good, alg_both)) + | (!fenrir_state(prF_dir, Auth, alg_both, alg_good)) | (!fenrir_state(prF_dir, Auth, alg_good, alg_good)) + | (!client_dir (pbF_dir, Auth, OTP)) | (!fenrir_dir (prF_dir, Auth)) + | phase 1; + (!service(OTP)) + | (!client_full (pbF_dir, Auth, alg_both, alg_both, OTP)) | (!client_full (pbF_dir, Auth, alg_bad, alg_both, OTP)) + | (!client_full (pbF_dir, Auth, alg_both, alg_bad, OTP)) | (!client_full (pbF_dir, Auth, alg_bad, alg_bad, OTP)) + | (!fenrir_full (prF_dir, Auth, alg_good, alg_good)) + | (!client_state(pbF_dir, Auth, alg_both, alg_both, OTP)) | (!client_state(pbF_dir, Auth, alg_bad, alg_both, OTP)) + | (!client_state(pbF_dir, Auth, alg_both, alg_bad, OTP)) | (!client_state(pbF_dir, Auth, alg_bad, alg_bad, OTP)) + | (!fenrir_state(prF_dir, Auth, alg_good, alg_good)) + | (!client_dir (pbF_dir, Auth, OTP)) | (!fenrir_dir (prF_dir, Auth)) + | phase 2; + (!service(OTP)) + | (!client_full (pbF_dir, Auth, alg_good, alg_good, OTP)) + | (!fenrir_full (prF_dir, Auth, alg_both, alg_both)) | (!fenrir_full (prF_dir, Auth, alg_bad, alg_both)) + | (!fenrir_full (prF_dir, Auth, alg_both, alg_bad)) | (!fenrir_full (prF_dir, Auth, alg_bad, alg_bad)) + | (!client_state(pbF_dir, Auth, alg_good, alg_good, OTP)) + | (!fenrir_state(prF_dir, Auth, alg_both, alg_both)) | (!fenrir_state(prF_dir, Auth, alg_bad, alg_both)) + | (!fenrir_state(prF_dir, Auth, alg_both, alg_bad)) | (!fenrir_state(prF_dir, Auth, alg_bad, alg_bad)) + | (!client_dir (pbF_dir, Auth, OTP)) | (!fenrir_dir (prF_dir, Auth)) +*) + ) + + + diff --git a/proverif/Fenrir_fix.pv b/proverif/Fenrir_fix.pv new file mode 100644 index 0000000..dc6d198 --- /dev/null +++ b/proverif/Fenrir_fix.pv @@ -0,0 +1,388 @@ + +(* + * Formal definition to verify the Fenrir protocol. + * to be used with ProVerif + * + * This is to verify the correctness of the full 3-RTT handshake. + * DNSSEC is NOT verified, as it is assumed to be correct. + * + * The test *WILL* take a while... proverif says it has inserted more than 23k rules, and has a rule base of more than 12k rules. + * just leave it to work... + *) + +(* + * ============== + * Type definition + * ============== + *) + + +type host. +type sKey. (* symmetric key *) +type pubKey. (* public key for asymmetric key encryption *) +type privKey. (* private key for asymmetric key encryption *) +type nonce. (* just a nonce *) + +const leak: channel. (* to leak private material *) +const cf_full: channel. (* client-fenrir, full-security handshake *) +const cf_state: channel. (* client-fenrir, stateful handshake *) +const cf_dir: channel. (* client-fenrir, directory-synchronized handshake *) +const cs: channel. (* client-service *) +const sf: channel [private]. (* service-fenrir: since it is managed as the client-fenrir channel, this is not checked *) +const C, F, S: host. (* Client, Fenrir, Service *) + +(* various stuff that should remain private *) +const leakCheck: bitstring [private]. +const Auth: nonce [private]. +const prF: privKey [private]. +const prF_dir: privKey [private]. +free fsKey: sKey [private]. + +free Rekey: bitstring. (* rekey message *) +type algorithm. +const alg_bad: algorithm. (* broken key exchange algorithm *) +const alg_good: algorithm. (* good key exchange algorithm *) +const alg_both: algorithm. (* both good and bad algorithms support*) + +(* + * ============== + * Function definition + * ============== + *) + +(* symmetric key encription *) +fun sEnc(bitstring, sKey): bitstring. (* encrypt with symmetric key *) +reduc forall c: bitstring, k: sKey; sDec(sEnc(c,k),k) = c. (* decrypt with symmetric key *) + +(* public key definition *) +fun genPub(privKey): pubKey. (* public keys are generated from private ones *) +fun aEnc(bitstring, pubKey): bitstring. (* encrypt with asymmetric public key *) +reduc forall c: bitstring, k: privKey; aDec(aEnc(c,genPub(k)),k) = c. (* decrypt with private key *) +(* public key signing *) +fun sign(bitstring, privKey): bitstring. +reduc forall c: bitstring, k: privKey; ver(c, sign(c, k), genPub(k)) = true. (* verify signature *) +(* integrity for encrypt then mac *) +fun int(bitstring, sKey): bitstring. +reduc forall c: bitstring, k: sKey; verint(c, int(c, k), k) = true. + +(* some key exchange based on public keys *) +fun exchange(privKey, pubKey) : sKey. +equation forall p1 : privKey, p2 : privKey; exchange(p1, genPub(p2)) = exchange(p2, genPub(p1)). + + + +(* + * ============== + * Events -- used for correlation + * ============== + *) +event downgrade(). +event acceptedClient(host, sKey). +event acceptedFenrir(host, sKey). +event acceptedClientState(host, sKey). +event acceptedFenrirState(host, sKey). +event clientConnect(host, host, sKey). +event serviceConnect(host, host, sKey). + + + +(* Deactivated because the complexity explodes... +let client_rekey (key: sKey, chan: channel) = + new rekey_p1: privKey; + new rekey_n1: nonce; + out (chan, sEnc((rekey_n1, genPub(rekey_p1)), key)); + in (chan, enc: bitstring); + let (=rekey_n1, srv_eph : pubKey) = sDec(enc, key) in + let (new_Key) = exchange(rekey_p1, srv_eph) in + out (chan, sEnc((Auth, Auth), new_Key)) + . + +let server_rekey (key: sKey, chan: channel) = + new rekey_s_p: privKey; + in (chan, enc: bitstring); + let (client_n1: nonce, client_p: pubKey) = sDec (enc, key) in + out (chan, sEnc((client_n1, genPub(rekey_s_p)), key)); + let (new_Key) = exchange(rekey_s_p, client_p) in + in (chan, enc2: bitstring); + let (=Auth, =Auth) = sDec(enc2, new_Key) + . +*) + +(* + * ========================================================================== + * Client definition, Full-security handshake with good and broken algorithms + * ========================================================================== + *) + +let client_full(pubF: pubKey, client: host, service: host, fenrir: host, Auth: nonce, supported: algorithm) = + new cn1: nonce; (* Client Nonce 1 *) + new prC: privKey; + + (* Note: this nonce is technically useless, but prevents amplification/DoS attack + * also: the nonce should include a timer, but proverif doesn't check for DoS, + * and doesn't play nicely with timers, so we don't really care... + *) +(* start cookie exchange *) + out (cf_full, (client, cn1, supported)); + in (cf_full, (sn1: nonce, selected: algorithm, s1: bitstring, s2: bitstring)); + if ver((sn1, cn1, supported, selected), s1, pubF) = true then + if ver((sn1, selected), s2, pubF) = true then + +(* RTT 1 completed *) + + (* start algorithm agreement *) + new cn2: nonce; + (* out: nonces and signature, supported_algorithms *) + (* bad algorithm somehow exposes authentication data *) + if selected = alg_bad && (supported = alg_both || supported = alg_bad) then + ( + event downgrade() + ) + else + ( + if selected = alg_good then + out (cf_full, (sn1, selected, s2, cn2, genPub(prC))); + (* se1: server encrypt 1: contains supported authentication algorithms + * unused here, it's the same mechanism as the "selected" one + *) + in (cf_full, (ephF: pubKey, se1: bitstring, s3: bitstring)); + if ver((ephF, se1), s3, pubF) = true then + let (cfKey) = exchange(prC, ephF) in +(* RTT 2 Completed *) + out (cf_full, (sEnc((Auth, Auth), cfKey))); + in (cf_full, (se2: bitstring)); + let (chan: channel, csKey: sKey) = sDec(se2, cfKey) in + event acceptedClient(client, cfKey); + +(* RTT 3 completed, can now connect to service *) +(* also send private data to test secrecy *) + + event clientConnect(service, client, csKey); + out (chan, sEnc((Auth, Auth), csKey)) + ). + +(* now rekey *) + +(* + * =========================================================================== + * Fenrir definition, full security handshake, with good and broken algorithms + * =========================================================================== + *) + +let fenrir_full(privF: privKey, fenrir: host, service: host, Auth: nonce, supported: algorithm) = + (* + * NOTE: we do not model the service <-> fenrir authentication, as that is just the same + * as the fenrir <-> client full security authentication. We assume fenrir and service already share a key + *) + + (* Nonce exchange *) + in (cf_full, (client: host, fin1: nonce, client_alg: algorithm)); + new s_nonce: nonce; + (* triggers "event downgrade()" in the client, no need to go further *) + (* bad only if both support bad *) + if client_alg = alg_bad && (supported = alg_bad || supported = alg_both) then + ( + out (cf_full, (s_nonce, alg_bad, sign((s_nonce, fin1, client_alg, alg_bad), privF), + sign((s_nonce, alg_bad), privF))) + ) + else + ( + if client_alg = alg_good || client_alg = alg_both then + out (cf_full, (s_nonce, alg_good, sign((s_nonce, fin1, client_alg, alg_good), privF), + sign((s_nonce, alg_good), privF))); +(* RTT 1 finished *) + in (cf_full, (=s_nonce, =alg_good, signed: bitstring, fin2: nonce, pubC: pubKey)); + if ver((s_nonce, alg_good), signed, genPub(privF)) = true then + new prF2: privKey; + let (cfKey) = exchange(prF2, pubC) in + out (cf_full, (genPub(prF2), sEnc((supported, supported), cfKey), sign((genPub(prF2), sEnc((s_nonce, s_nonce), cfKey)), privF))); +(* RTT 2 finished, now we have a state *) + in (cf_full, (ce1: bitstring)); + let (data: nonce, data2: nonce) = sDec(ce1, cfKey) in + if data = Auth && data2 = Auth then + new csKey: sKey; + out (sf, (client, csKey)); (* inform service of new client *) + event acceptedFenrir(client, cfKey); + let (se1) = sEnc((cs, csKey), cfKey) in + out (cf_full, (sEnc((cs, csKey), cfKey))) +(* RT3 finished *) + ). + +(* + * ================================== + * Service definition, common for all + * ================================== + *) + +let service(service: host) = + in (sf, (cli: host, csKey:sKey)); + in (cs, enc2 : bitstring); + let (Auth1 : nonce, Auth2 : nonce) = sDec(enc2, csKey) in + event serviceConnect(service, cli, csKey). + + +(* + * ====================================================================== + * Client Definition, Stateful handshake, with good and broken algorithms + * ====================================================================== + *) + +let client_state (pubF: pubKey, client: host, service: host, fenrir: host, Auth: nonce, supported: algorithm) = + new cn1: nonce; (* Client Nonce 1 *) + new prC: privKey; + + (* Note: this nonce is technically useless, but prevents amplification/DoS attack + * also: the nonce should include a timer, but proverif doesn't check for DoS, + * and doesn't play nicely with timers, so we don't really care... + *) +(* start cookie exchange *) + out (cf_state, (cn1, client, supported)); + in (cf_state, (alg: algorithm, ephF: pubKey, s1: bitstring)); + if ver((cn1, client, supported, alg, ephF), s1, pubF) = true then + +(* RTT 1 completed *) + + if alg = alg_bad then + ( + if supported = alg_bad || supported = alg_both then + (* bad algorithm exposes authentication data *) + event downgrade() + ) + else + ( + if alg = alg_good then + if supported = alg_good || supported = alg_both then + + let (cfKey) = exchange(prC, ephF) in + out (cf_state, (genPub(prC), sEnc((Auth,Auth), cfKey))); + in (cf_state, enc: bitstring); + let (chan : channel, csKey : sKey) = sDec(enc, cfKey) in + event acceptedClientState(client, csKey); + +(* RTT 2 completed, can now connect to service *) +(* also send private data to test secrecy *) + + event clientConnect(service, client, csKey); + out (chan, sEnc((Auth, Auth), csKey)) + ). + +(* + * =========================================================================== + * Fenrir definition, stateful handshake, with good and broken algorithms + * =========================================================================== + *) + +let fenrir_state (privF: privKey, fenrir: host, service: host, Auth: nonce, supported: algorithm) = + (* + * NOTE: we do not model the service <-> fenrir authentication, as that is just the same + * as the fenrir <-> client full-securoty authentication. We assume fenrir and service already share a key + *) + + (* Nonce exchange *) + new prF2 : privKey; + new s_nonce: nonce; + in (cf_state, (fin1: nonce, client: host, client_alg: algorithm)); + if client_alg = alg_bad && (supported = alg_bad || supported = alg_both) then + ( + out(cf_state, (alg_bad, genPub(prF2), sign((fin1, client, client_alg, alg_bad, genPub(prF2)), privF))) + ) + else + ( + if (client_alg = alg_good || client_alg = alg_both) && (supported = alg_good || supported = alg_both) then + out(cf_state, (alg_good, genPub(prF2), sign((fin1, client, client_alg, alg_good, genPub(prF2)), privF))); +(* RTT 1 finished *) + new csKey: sKey; + in (cf_state, (pubC: pubKey, enc: bitstring)); + let (cfKey) = exchange(prF2, pubC) in + let (data: nonce, data2: nonce) = sDec(enc, cfKey) in + if data = Auth && data2 = Auth then + out (sf, (client, csKey)); (* inform service of new client *) + event acceptedFenrirState(client, csKey); + out (cf_state, sEnc((cs, csKey), cfKey)) +(* RTT 2 finished *) + ). + + +(* + * =========================================================================== + * Client definition, directory synchronized handshake + * =========================================================================== + *) +let client_dir (pubF: pubKey, client: host, service: host, fenrir: host, Auth: nonce) = + new prC : privKey; + new cn : nonce; + let (cfKey) = exchange(prC, pubF) in + out (cf_dir, (genPub(prC), sEnc((client, Auth,cn), cfKey))); + in (cf_dir, enc: bitstring); + let (=cn, chan: channel, csKey: sKey) = sDec(enc, cfKey) in +(* RTT 1 finished, now connect to service *) + out (chan, sEnc((Auth, Auth), csKey)). +(* + * =========================================================================== + * Fenrir definition, directory synchronized handshake + * =========================================================================== + *) + +let fenrir_dir (privF: privKey, fenrir: host, service: host, Auth: nonce) = + in (cf_dir, (pubC: pubKey, enc: bitstring)); + let (cfKey) = exchange(privF, pubC) in + let (cname: host, =Auth, cn: nonce) = sDec (enc, cfKey) in + + new csKey : sKey; + out (sf, sEnc((cname, csKey), fsKey)); (* inform service of new client *) + out (cf_dir, sEnc((cn, cs, csKey), cfKey)). +(* + * Event correlation: + *) +(* query h: host, k: sKey; event(acceptedFenrir(h, k)) ==> event(acceptedClient(h, k)). *) +(* *) +query h: host, k: sKey; event(acceptedClientState(h, k)) ==> event(acceptedFenrirState(h, k)). +query h1: host, h2 : host, k: sKey, t: nonce; event(serviceConnect(h1, h2, k)) ==> event(clientConnect(h1, h2, k)). + + +(* + * ============== + * What should be secret? + * ============== + *) + +(*query attacker(prF). do NOT check this as we volountarly leak it after the process *) +(*query attacker(prF_dir).*) (* the private key in the directory-synchronized case must be secret *) +query attacker(Auth). (* client auth data. *) +query event(downgrade()). +(* + * ============== + * Run the verification + * ============== + *) + +(* make it easy to deactivate single parts, like the 2-RTT login, which has unproven events problems *) + +(* TODO: fix PFS: must leak both server and client public key *) +process + let pbF = genPub(prF) in + let pbF_dir = genPub(prF_dir) in + ( (!service(S)) + | (!client_full (pbF, C, S, F, Auth, alg_both)) | (!client_full (pbF, C, S, F, Auth, alg_good)) + | (!fenrir_full (prF, F, S, Auth, alg_both)) | (!fenrir_full (prF, F, S, Auth, alg_good)) + | (!client_state(pbF, C, S, F, Auth, alg_both)) | (!client_state(pbF, C, S, F, Auth, alg_good)) + | (!fenrir_state(prF, F, S, Auth, alg_both)) | (!fenrir_state(prF, F, S, Auth, alg_good)) + | (!client_dir (pbF_dir, C, S, F, Auth)) | (!fenrir_dir (prF, F, S, Auth)) + | phase 1; out(leak, prF) (* PFS: leaking of the long-term secret will NOT affect previous communications *) + (* Now do everything again, WITHOUT leaking. Everything must be done again since + * we leaked the previous private key. If we didn't do everything again we could not prove + * that the interaction of the handshakes is secure. + * This is because the 1-RTT handshake does NOT have long-term secret + *) + + ; (!client_full (pbF_dir, C, S, F, Auth, alg_both)) | (!client_full (pbF_dir, C, S, F, Auth, alg_good)) + | (!fenrir_full (prF_dir, F, S, Auth, alg_both)) | (!fenrir_full (prF_dir, F, S, Auth, alg_good)) + | (!client_state(pbF_dir, C, S, F, Auth, alg_both)) | (!client_state(pbF_dir, C, S, F, Auth, alg_good)) + | (!fenrir_state(prF_dir, F, S, Auth, alg_both)) | (!fenrir_state(prF_dir, F, S, Auth, alg_good)) + | (!client_dir (pbF_dir, C, S, F, Auth)) | (!fenrir_dir (prF_dir, F, S, Auth)) + + ) + + + + diff --git a/proverif/Fenrir_old.pv b/proverif/Fenrir_old.pv new file mode 100644 index 0000000..f01b62c --- /dev/null +++ b/proverif/Fenrir_old.pv @@ -0,0 +1,378 @@ + +(* + * Formal definition to verify the Fenrir protocol. + * to be used with ProVerif + * + * This is to verify the correctness of the full 3-RTT handshake. + * DNSSEC is NOT verified, as it is assumed to be correct. + * + * The test *WILL* take a while... proverif says it has inserted more than 23k rules, and has a rule base of more than 12k rules. + * just leave it to work... + *) + +(* + * ============== + * Type definition + * ============== + *) + + +type host. +type sKey. (* symmetric key *) +type pubKey. (* public key for asymmetric key encryption *) +type privKey. (* private key for asymmetric key encryption *) +type nonce. (* just a nonce *) + +const leak: channel. (* to leak private material *) +const cf_full: channel. (* client-fenrir, full-security handshake *) +const cf_state: channel. (* client-fenrir, stateful handshake *) +const cf_dir: channel. (* client-fenrir, directory-synchronized handshake *) +const cs: channel. (* client-service *) +const sf: channel [private]. (* service-fenrir: since it is managed as the client-fenrir channel, this is not checked *) +const C, F, S: host. (* Client, Fenrir, Service *) + +(* various stuff that should remain private *) +const leakCheck: bitstring [private]. +const Auth: nonce [private]. +const prF: privKey [private]. +const prF_dir: privKey [private]. +free fsKey: sKey [private]. + +free Rekey: bitstring. (* rekey message *) +type algorithm. +const alg_bad: algorithm. (* broken key exchange algorithm *) +const alg_good: algorithm. (* good key exchange algorithm *) +const alg_both: algorithm. (* both good and bad algorithms support*) + +(* + * ============== + * Function definition + * ============== + *) + +(* symmetric key encription *) +fun sEnc(bitstring, sKey): bitstring. (* encrypt with symmetric key *) +reduc forall c: bitstring, k: sKey; sDec(sEnc(c,k),k) = c. (* decrypt with symmetric key *) + +(* public key definition *) +fun genPub(privKey): pubKey. (* public keys are generated from private ones *) +fun aEnc(bitstring, pubKey): bitstring. (* encrypt with asymmetric public key *) +reduc forall c: bitstring, k: privKey; aDec(aEnc(c,genPub(k)),k) = c. (* decrypt with private key *) +(* public key signing *) +fun sign(bitstring, privKey): bitstring. +reduc forall c: bitstring, k: privKey; ver(c, sign(c, k), genPub(k)) = true. (* verify signature *) + +(* some key exchange based on public keys *) +fun exchange(privKey, pubKey) : sKey. +equation forall p1 : privKey, p2 : privKey; exchange(p1, genPub(p2)) = exchange(p2, genPub(p1)). + + + +(* + * ============== + * Events -- used for correlation + * ============== + *) +event downgrade(). +event acceptedClient(host, sKey). +event acceptedFenrir(host, sKey). +event acceptedClientState(host, sKey). +event acceptedFenrirState(host, sKey). +event clientConnect(host, host, sKey). +event serviceConnect(host, host, sKey). + + + +(* Deactivated because the complexity explodes... +let client_rekey (key: sKey, chan: channel) = + new rekey_p1: privKey; + new rekey_n1: nonce; + out (chan, sEnc((rekey_n1, genPub(rekey_p1)), key)); + in (chan, enc: bitstring); + let (=rekey_n1, srv_eph : pubKey) = sDec(enc, key) in + let (new_Key) = exchange(rekey_p1, srv_eph) in + out (chan, sEnc((Auth, Auth), new_Key)) + . + +let server_rekey (key: sKey, chan: channel) = + new rekey_s_p: privKey; + in (chan, enc: bitstring); + let (client_n1: nonce, client_p: pubKey) = sDec (enc, key) in + out (chan, sEnc((client_n1, genPub(rekey_s_p)), key)); + let (new_Key) = exchange(rekey_s_p, client_p) in + in (chan, enc2: bitstring); + let (=Auth, =Auth) = sDec(enc2, new_Key) + . +*) + +(* + * ========================================================================== + * Client definition, Full-security handshake with good and broken algorithms + * ========================================================================== + *) + +let client_full(pubF: pubKey, client: host, service: host, fenrir: host, Auth: nonce, supported: algorithm) = + new cn1: nonce; (* Client Nonce 1 *) + new prC: privKey; + + (* Note: this nonce is technically useless, but prevents amplification/DoS attack + * also: the nonce should include a timer, but proverif doesn't check for DoS, + * and doesn't play nicely with timers, so we don't really care... + *) +(* start cookie exchange *) + out (cf_full, (client, cn1)); + in (cf_full, (sn1: nonce , s1: bitstring)); + if ver((sn1, cn1), s1, pubF) = true then + +(* RTT 1 completed *) + + (* start algorithm agreement *) + new cn2: nonce; + (* out: nonces and signature, supported_algorithms *) + out (cf_full, (cn2, cn1, sn1, s1, supported)); + in (cf_full, (selected: algorithm, ephF : pubKey, s2 : bitstring)); + + if ver((supported, selected, ephF, cn2), s2, pubF) then + if selected = alg_bad && (supported = alg_both || supported = alg_bad) then + ( + (* bad algorithm somehow exposes authentication data *) + event downgrade() + ) + else + ( + if selected = alg_good then + +(* RTT 2 completed *) + + let (cfKey) = exchange(prC, ephF) in + out (cf_full, (genPub(prC), sEnc((Auth,Auth), cfKey))); + in (cf_full, enc: bitstring); + let (chan : channel, csKey : sKey) = sDec(enc, cfKey) in + event acceptedClient(client, cfKey); + +(* RTT 3 completed, can now connect to service *) +(* also send private data to test secrecy *) + + event clientConnect(service, client, csKey); + out (chan, sEnc((Auth, Auth), csKey)) + ). + +(* now rekey *) + +(* + * =========================================================================== + * Fenrir definition, full security handshake, with good and broken algorithms + * =========================================================================== + *) + +let fenrir_full(privF: privKey, fenrir: host, service: host, Auth: nonce, supported: algorithm) = + (* + * NOTE: we do not model the service <-> fenrir authentication, as that is just the same + * as the fenrir <-> client full security authentication. We assume fenrir and service already share a key + *) + + (* Nonce exchange *) + in (cf_full, (client: host, fin1: nonce)); + new s_nonce: nonce; + out(cf_full, (s_nonce, sign((s_nonce, fin1), privF))); +(* RTT 1 finished *) + + in (cf_full, (fin2: nonce, fin1_1: nonce, srv_n: nonce, signature: bitstring, client_alg: algorithm)); + if ver((srv_n, fin1_1), signature, genPub(privF)) = true then + new prF2 : privKey; + new csKey: sKey; + if client_alg = alg_bad && (supported = alg_bad || supported = alg_both) then + ( (* bad only if both support bad *) + out (cf_full, (alg_bad, genPub(prF2), sign((client_alg, alg_bad, genPub(prF2), fin2), privF))) + ) + else + ( + if (client_alg = alg_good || client_alg = alg_both) && (supported = alg_good || supported = alg_both) then + out (cf_full, (alg_good, genPub(prF2), sign((client_alg, alg_good, genPub(prF2), fin2), privF))); +(* RTT 2 finished *) + in (cf_full, (pubC: pubKey, enc: bitstring)); + let (cfKey) = exchange(prF2, pubC) in + let (data: nonce, data2: nonce) = sDec(enc, cfKey) in + if data = Auth && data2 = Auth then + out (sf, (client, csKey)); (* inform service of new client *) + event acceptedFenrir(client, cfKey); + out (cf_full, sEnc((cs, csKey), cfKey)) +(* RTT 3 finished *) + ). + +(* + * ================================== + * Service definition, common for all + * ================================== + *) + +let service(service: host) = + in (sf, (cli: host, csKey:sKey)); + in (cs, enc2 : bitstring); + let (Auth1 : nonce, Auth2 : nonce) = sDec(enc2, csKey) in + event serviceConnect(service, cli, csKey). + + +(* + * ====================================================================== + * Client Definition, Stateful handshake, with good and broken algorithms + * ====================================================================== + *) + +let client_state (pubF: pubKey, client: host, service: host, fenrir: host, Auth: nonce, supported: algorithm) = + new cn1: nonce; (* Client Nonce 1 *) + new prC: privKey; + + (* Note: this nonce is technically useless, but prevents amplification/DoS attack + * also: the nonce should include a timer, but proverif doesn't check for DoS, + * and doesn't play nicely with timers, so we don't really care... + *) +(* start cookie exchange *) + out (cf_state, (cn1, client, supported)); + in (cf_state, (alg: algorithm, ephF: pubKey, s1: bitstring)); + if ver((cn1, client, supported, alg, ephF), s1, pubF) = true then + +(* RTT 1 completed *) + + if alg = alg_bad then + ( + if supported = alg_bad || supported = alg_both then + (* bad algorithm exposes authentication data *) + event downgrade() + ) + else + ( + if alg = alg_good then + if supported = alg_good || supported = alg_both then + + let (cfKey) = exchange(prC, ephF) in + out (cf_state, (genPub(prC), sEnc((Auth,Auth), cfKey))); + in (cf_state, enc: bitstring); + let (chan : channel, csKey : sKey) = sDec(enc, cfKey) in + event acceptedClientState(client, csKey); + +(* RTT 2 completed, can now connect to service *) +(* also send private data to test secrecy *) + + event clientConnect(service, client, csKey); + out (chan, sEnc((Auth, Auth), csKey)) + ). + +(* + * =========================================================================== + * Fenrir definition, stateful handshake, with good and broken algorithms + * =========================================================================== + *) + +let fenrir_state (privF: privKey, fenrir: host, service: host, Auth: nonce, supported: algorithm) = + (* + * NOTE: we do not model the service <-> fenrir authentication, as that is just the same + * as the fenrir <-> client full-securoty authentication. We assume fenrir and service already share a key + *) + + (* Nonce exchange *) + new prF2 : privKey; + new s_nonce: nonce; + in (cf_state, (fin1: nonce, client: host, client_alg: algorithm)); + if client_alg = alg_bad && (supported = alg_bad || supported = alg_both) then + ( + out(cf_state, (alg_bad, genPub(prF2), sign((fin1, client, client_alg, alg_bad, genPub(prF2)), privF))) + ) + else + ( + if (client_alg = alg_good || client_alg = alg_both) && (supported = alg_good || supported = alg_both) then + out(cf_state, (alg_good, genPub(prF2), sign((fin1, client, client_alg, alg_good, genPub(prF2)), privF))); +(* RTT 1 finished *) + new csKey: sKey; + in (cf_state, (pubC: pubKey, enc: bitstring)); + let (cfKey) = exchange(prF2, pubC) in + let (data: nonce, data2: nonce) = sDec(enc, cfKey) in + if data = Auth && data2 = Auth then + out (sf, (client, csKey)); (* inform service of new client *) + event acceptedFenrirState(client, csKey); + out (cf_state, sEnc((cs, csKey), cfKey)) +(* RTT 2 finished *) + ). + + +(* + * =========================================================================== + * Client definition, directory synchronized handshake + * =========================================================================== + *) +let client_dir (pubF: pubKey, client: host, service: host, fenrir: host, Auth: nonce) = + new prC : privKey; + new cn : nonce; + let (cfKey) = exchange(prC, pubF) in + out (cf_dir, (genPub(prC), sEnc((client, Auth,cn), cfKey))); + in (cf_dir, enc: bitstring); + let (=cn, chan: channel, csKey: sKey) = sDec(enc, cfKey) in +(* RTT 1 finished, now connect to service *) + out (chan, sEnc((Auth, Auth), csKey)). +(* + * =========================================================================== + * Fenrir definition, directory synchronized handshake + * =========================================================================== + *) + +let fenrir_dir (privF: privKey, fenrir: host, service: host, Auth: nonce) = + in (cf_dir, (pubC: pubKey, enc: bitstring)); + let (cfKey) = exchange(privF, pubC) in + let (cname: host, =Auth, cn: nonce) = sDec (enc, cfKey) in + + new csKey : sKey; + out (sf, sEnc((cname, csKey), fsKey)); (* inform service of new client *) + out (cf_dir, sEnc((cn, cs, csKey), cfKey)). +(* + * Event correlation: + *) +(* query h: host, k: sKey; event(acceptedFenrir(h, k)) ==> event(acceptedClient(h, k)). *) +(* *) +query h: host, k: sKey; event(acceptedClientState(h, k)) ==> event(acceptedFenrirState(h, k)). +query h1: host, h2 : host, k: sKey, t: nonce; event(serviceConnect(h1, h2, k)) ==> event(clientConnect(h1, h2, k)). + + +(* + * ============== + * What should be secret? + * ============== + *) + +(*query attacker(prF). do NOT check this as we volountarly leak it after the process *) +(*query attacker(prF_dir).*) (* the private key in the directory-synchronized case must be secret *) +query attacker(Auth). (* client auth data. *) +query event(downgrade()). +(* + * ============== + * Run the verification + * ============== + *) + +(* make it easy to deactivate single parts, like the 2-RTT login, which has unproven events problems *) + +(* TODO: fix PFS: must leak both server and client public key *) +process + let pbF = genPub(prF) in + let pbF_dir = genPub(prF_dir) in + ( (!service(S)) + | (!client_full (pbF, C, S, F, Auth, alg_both)) | (!client_full (pbF, C, S, F, Auth, alg_good)) + | (!fenrir_full (prF, F, S, Auth, alg_both)) | (!fenrir_full (prF, F, S, Auth, alg_good)) + | (!client_state(pbF, C, S, F, Auth, alg_both)) | (!client_state(pbF, C, S, F, Auth, alg_good)) + | (!fenrir_state(prF, F, S, Auth, alg_both)) | (!fenrir_state(prF, F, S, Auth, alg_good)) + | (!client_dir (pbF_dir, C, S, F, Auth)) | (!fenrir_dir (prF, F, S, Auth)) + | phase 1; out(leak, prF) (* PFS: leaking of the long-term secret will NOT affect previous communications *) + (* Now do everything again, WITHOUT leaking. Everything must be done again since + * we leaked the previous private key. If we didn't do everything again we could not prove + * that the interaction of the handshakes is secure. + * This is because the 1-RTT handshake does NOT have long-term secret + *) +(* ; (!client_full (pbF, C, S, F, Auth, alg_both)) | (!client_full (pbF, C, S, F, Auth, alg_good)) + | (!fenrir_full (prF, F, S, Auth, alg_both)) | (!fenrir_full (prF, F, S, Auth, alg_good)) + | (!client_state(pbF, C, S, F, Auth, alg_both)) | (!client_state(pbF, C, S, F, Auth, alg_good)) + | (!fenrir_state(prF, F, S, Auth, alg_both)) | (!fenrir_state(prF, F, S, Auth, alg_good)) + | (!client_dir (pbF_dir, C, S, F, Auth)) | (!fenrir_dir (prF_dir, F, S, Auth)) *) + ) + + + + diff --git a/proverif/RogueAS.pv b/proverif/RogueAS.pv new file mode 100644 index 0000000..1e15d6f --- /dev/null +++ b/proverif/RogueAS.pv @@ -0,0 +1,176 @@ + +(* + * Formal definition to verify the Fenrir protocol. + * to be used with ProVerif + * + * Here we check the security of the connection between client + * and service in the case of a compromised authentication server + *) + +(* + * ============== + * Type definition + * ============== + *) + +type pubKey. (* public key for asymmetric key encryption *) +type privKey. (* private key for asymmetric key encryption *) +type sKey. (* symmetric key *) +type nonce. (* just a nonce *) + +const cs: channel. (* simulates service-fenrir channel for authentication *) + +(* various stuff that should remain private *) +const prS: privKey [private]. (* service private key *) +free csKey: sKey [private]. +free shared: sKey [private]. + + +(* + * ============== + * Function definition + * ============== + *) + +(* key to bitstring conversion *) +fun fromKey(sKey) : bitstring. +reduc forall a : sKey; toKey(fromKey(a)) = a. + + +(* symmetric key encription *) +fun sEnc(bitstring, sKey): bitstring. (* encrypt with symmetric key *) +reduc forall c: bitstring, k: sKey; sDec(sEnc(c,k),k) = c. (* decrypt with symmetric key *) + +(* public key definition *) +fun genPub(privKey): pubKey. (* public keys are generated from private ones *) +(* public key signing *) +fun sign(bitstring, privKey): bitstring. +reduc forall c: bitstring, k: privKey; ver(c, sign(c, k), genPub(k)) = true. (* verify signature *) + +(* some key exchange based on public keys *) +fun exchange(privKey, pubKey) : sKey. +equation forall p1 : privKey, p2 : privKey; exchange(p1, genPub(p2)) = exchange(p2, genPub(p1)). + +(* hash used by OTP, sKey based *) +fun hash(sKey) : sKey. + +(* xor function *) +(* note: this xor function doe not handle associativity as proverif would loop, + * so we pay attention to use it in a way that does not require associativity + *) +fun xor(sKey, sKey) : sKey. +reduc forall a : sKey, b : sKey; unxor(xor(a, b), b) = a. +reduc forall a : sKey, b : sKey; unxor2(xor(a, b), a) = b. (* created for proverif, not used for simplicity *) + + +(* + * ============== + * Events -- used for correlation + * ============== + *) +event clientConnect(sKey). +event serviceConnect(sKey). + + +(* rekeying algorithm *) + +let client_rekey (key: sKey, chan: channel, pb : pubKey) = + new rekey_p1: privKey; + new rekey_n1: nonce; + out (chan, sEnc((rekey_n1, genPub(rekey_p1)), key)); + in (chan, enc: bitstring); + let (=rekey_n1, srv_eph : pubKey, signed : bitstring) = sDec(enc, key) in + if ver((rekey_n1, srv_eph), signed, pb) then + let (new_Key) = exchange(rekey_p1, srv_eph) in + out (chan, sEnc((shared, shared), new_Key)) (* test secrecy *) + . + +let server_rekey (key: sKey, chan: channel, pr : privKey) = + new rekey_s_p: privKey; + in (chan, enc: bitstring); + let (client_n1: nonce, client_p: pubKey) = sDec (enc, key) in + out (chan, sEnc((client_n1, genPub(rekey_s_p), sign((client_n1, genPub(rekey_s_p)), pr)), key)); + let (new_Key) = exchange(rekey_s_p, client_p) in + in (chan, enc2: bitstring); + let (=shared, =shared) = sDec(enc2, new_Key) + . + + +(* test the connection between the service and client. Assume that the authentication server + * has been compromised. *) + + +let service_shared() = + let xored = xor(csKey, shared) in + out (cs, xored); + in (cs, enc : bitstring); + let data = sDec(enc, csKey) in + if data = fromKey(shared) then + event clientConnect(csKey); + server_rekey(csKey, cs, prS). + +let client_shared(pbS: pubKey) = + in (cs, xored : sKey); + let xorKey = unxor(xored, shared) in + event serviceConnect(xorKey); + out (cs, sEnc(fromKey(shared), xorKey)); (* test 'shared' secrecy *) + client_rekey(xorKey, cs, pbS). + + +(* assume that the client and service have not yet setup a shared secret *) +(* DATA is the secret data *) + +let service_no_shared() = + in (cs, pbC : pubKey); + let shared2 = exchange(prS, pbC) in + let xored = xor(csKey, shared2) in + out (cs, xored); + in (cs, enc : bitstring); + let data = sDec(enc, csKey) in + if data = fromKey(shared) then + event clientConnect(csKey); + server_rekey(csKey, cs, prS). + +let client_no_shared(pbS: pubKey) = + new prC : privKey; + out (cs, genPub(prC)); + let shared2 = exchange(prC, pbS) in + in (cs, xored : sKey); + let xorKey = unxor(xored, shared2) in + event serviceConnect(xorKey); + out (cs, sEnc(fromKey(shared), xorKey)); (* test 'shared' secrecy *) + client_rekey(xorKey, cs, pbS). + + +(* assume that the client and service have not yet setup a shared secret *) +(* DATA is the secret data *) + +(* + * Event correlation: + *) +query k : sKey; event(clientConnect(k)) ==> event(serviceConnect(k)). + +(* + * ============== + * What should be secret? + * ============== + *) + +query attacker(shared). (* client-service shared key. *) +query attacker(csKey). (* client-service key. *) + +(* + * ============== + * Run the verification + * ============== + *) + +(* make it easy to deactivate single parts, like the 2-RTT login, which has unproven events problems *) + +process + (!service_no_shared()) | (!client_no_shared(genPub(prS))) + | phase 1; (!service_shared()) | (!client_shared(genPub(prS))) + + + + diff --git a/proverif/RogueAS_otp.pv b/proverif/RogueAS_otp.pv new file mode 100644 index 0000000..dddb47e --- /dev/null +++ b/proverif/RogueAS_otp.pv @@ -0,0 +1,187 @@ + +(* + * Formal definition to verify the Fenrir protocol. + * to be used with ProVerif + * + * This is to verify the correctness of the full 3-RTT handshake. + * DNSSEC is NOT verified, as it is assumed to be correct. + * + * compared to the handshakes, we have a lot less to check, so the tests are very quick + *) + +(* + * ============== + * Type definition + * ============== + *) + +type pubKey. (* public key for asymmetric key encryption *) +type privKey. (* private key for asymmetric key encryption *) +type sKey. (* symmetric key *) +type nonce. (* just a nonce *) + +const leak: channel. (* to leak private material *) +const cs_xor: channel. (* service-fenrir channel for xor otp auth *) + +(* various stuff that should remain private *) +const prS: privKey [private]. (* service private key *) +const OTP: sKey [private]. +free csKey: sKey [private]. + + +(* + * ============== + * Function definition + * ============== + *) + +(* any to bitstring conversion *) +fun fromKey(sKey) : bitstring. +reduc forall a : sKey; toKey(fromKey(a)) = a. + + +(* symmetric key encription *) +fun sEnc(bitstring, sKey): bitstring. (* encrypt with symmetric key *) +reduc forall c: bitstring, k: sKey; sDec(sEnc(c,k),k) = c. (* decrypt with symmetric key *) + +(* public key definition *) +fun genPub(privKey): pubKey. (* public keys are generated from private ones *) +fun aEnc(bitstring, pubKey): bitstring. (* encrypt with asymmetric public key *) +reduc forall c: bitstring, k: privKey; aDec(aEnc(c,genPub(k)),k) = c. (* decrypt with private key *) +(* public key signing *) +fun sign(bitstring, privKey): bitstring. +reduc forall c: bitstring, k: privKey; ver(c, sign(c, k), genPub(k)) = true. (* verify signature *) +(* integrity for encrypt then mac *) +fun int(bitstring, sKey): bitstring. +reduc forall c: bitstring, k: sKey; verint(c, int(c, k), k) = true. + +(* some key exchange based on public keys *) +fun exchange(privKey, pubKey) : sKey. +equation forall p1 : privKey, p2 : privKey; exchange(p1, genPub(p2)) = exchange(p2, genPub(p1)). + +(* hash used by OTP, sKey based *) +fun hash(sKey) : sKey. + +(* xor function *) +(* note: this xor function doe not handle associativity as proverif would loop, + * so we pay attention to use it in a way that does not require associativity + *) +fun xor(sKey, sKey) : sKey. +reduc forall a : sKey, b : sKey; unxor(xor(a, b), b) = a. +reduc forall a : sKey, b : sKey; unxor2(xor(a, b), a) = b. (* created for proverif, not used for simplicity *) + + +(* + * ============== + * Events -- used for correlation + * ============== + *) +event clientConnect(sKey). +event serviceConnect(sKey). + + +(* rekeying algorithm *) + +let client_rekey (key: sKey, chan: channel, pb : pubKey) = + new rekey_p1: privKey; + new rekey_n1: nonce; + out (chan, sEnc((rekey_n1, genPub(rekey_p1)), key)); + in (chan, enc: bitstring); + let (=rekey_n1, srv_eph : pubKey, signed : bitstring) = sDec(enc, key) in + if ver((rekey_n1, srv_eph), signed, pb) then + let (new_Key) = exchange(rekey_p1, srv_eph) in + out (chan, sEnc((OTP, OTP), new_Key)) (* test secrecy *) + . + +let server_rekey (key: sKey, chan: channel, pr : privKey) = + new rekey_s_p: privKey; + in (chan, enc: bitstring); + let (client_n1: nonce, client_p: pubKey) = sDec (enc, key) in + out (chan, sEnc((client_n1, genPub(rekey_s_p), sign((client_n1, genPub(rekey_s_p)), pr)), key)); + let (new_Key) = exchange(rekey_s_p, client_p) in + in (chan, enc2: bitstring); + let (=OTP, =OTP) = sDec(enc2, new_Key) + . + + +(* test the OTP between the service and client. Assume that the authentication server + * has been compromised. *) + +(* assume that the client and service have not yet setup an OTP *) + +let service_no_otp() = + (* this first sent/received messages are relayed to the service/client by the AS *) + in (cs_xor, (enc: bitstring, pb: pubKey)); + let key = exchange(prS, pb) in + let bitOTP = sDec(enc, key) in + let sOTP = toKey(bitOTP) in + (* this should be cskey XOR hash(OTP), but proverif can't handle XOR. + * so we treat it as encryption, as it has the same properties in our case *) + let xored = xor(csKey, hash(sOTP)) in + out (cs_xor, xored); + in (cs_xor, enc2 : bitstring); + let is_OTP = sDec(enc2, csKey) in + if sOTP = toKey(is_OTP) then + event clientConnect(csKey); + server_rekey(csKey, cs_xor, prS). + +let client_no_otp(OTP: sKey, pbS: pubKey) = + (* this first message is actually sent to the AS, but gets relayed to the service *) + new pr : privKey; + out (cs_xor, sEnc(fromKey(OTP), exchange(pr, pbS))); + in (cs_xor, xored : sKey); + let xorKey = unxor(xored, hash(OTP)) in + event serviceConnect(xorKey); + out (cs_xor, sEnc(fromKey(OTP), xorKey)); + client_rekey(xorKey, cs_xor, pbS). + +(* now assume that there is a shared OTP *) + +let service_otp(OTP : sKey) = + (* this should be cskey XOR hash(OTP), but proverif can't handle XOR. + * so we treat it as encryption, as it has the same properties in our case *) + let xorK = sEnc(fromKey(csKey), hash(OTP)) in + out (cs_xor, (xorK, xorK)); + in (cs_xor, enc2 : bitstring); + let is_OTP = sDec(enc2, csKey) in + if OTP = toKey(is_OTP) then + event clientConnect(csKey); + server_rekey(csKey, cs_xor, prS). + +let client_otp(OTP: sKey, pbS: pubKey) = + in (cs_xor, enc : bitstring); + let xorKey = sDec(enc, hash(OTP)) in + event serviceConnect(toKey(xorKey)); + out (cs_xor, sEnc(fromKey(OTP), toKey(xorKey))); + client_rekey(toKey(xorKey), cs_xor, pbS). + + +(* + * Event correlation: + *) +query k : sKey; event(clientConnect(k)) ==> event(serviceConnect(k)). + +(* + * ============== + * What should be secret? + * ============== + *) + +query attacker(OTP). (* client-service OTP data. *) + +(* + * ============== + * Run the verification + * ============== + *) + +(* make it easy to deactivate single parts, like the 2-RTT login, which has unproven events problems *) + +(* TODO: fix PFS: must leak both server and client public key *) +process + (!service_no_otp()) | (!client_no_otp(OTP, genPub(prS))) + | phase 1; (!service_otp(OTP)) | (!client_otp(OTP, genPub(prS))) + + + + diff --git a/proverif/colored_proverif.sh b/proverif/colored_proverif.sh new file mode 100755 index 0000000..e64135f --- /dev/null +++ b/proverif/colored_proverif.sh @@ -0,0 +1 @@ +proverif -color -in pitype $1|GREP_COLOR='01;32' egrep --line-buffered --color=always -E "^|attacker\(.*\)"|GREP_COLOR='01;36' egrep -i --line-buffered --color=always -E "^|message \(.*\)"|GREP_COLOR='01;31' egrep --line-buffered --color=always -E "|^RESULT.*" diff --git a/proverif/xor_test.pv b/proverif/xor_test.pv new file mode 100644 index 0000000..768c2b3 --- /dev/null +++ b/proverif/xor_test.pv @@ -0,0 +1,60 @@ + +(* + * Formal definition to verify the Fenrir protocol. + * to be used with ProVerif + * + * quick test to show that proverif can find xor keys + * even without associativity. + *) + +(* + * ============== + * Type definition + * ============== + *) + +type sKey. (* symmetric key *) + +const cs: channel. + +(* xor function *) +(* note: this xor function doe not handle associativity as proverif would loop, + * so we pay attention to use it in a way that does not require full associativity + *) +fun xor(sKey, sKey) : sKey. +reduc forall a : sKey, b : sKey; unxor(xor(a, b), b) = a. +reduc forall a : sKey, b : sKey; unxor2(xor(a, b), a) = b. (* created for proverif, not used for simplicity *) + + +const plain1: sKey [private]. +const plain2: sKey [private]. +(* keep the secret secret, or not? +free secret: sKey [private]. +free secret: sKey . +*) +free secret: sKey. + +let client1 (pl: sKey, sec: sKey) = + let xored = xor(pl, sec) in + out (cs, (xored)). +let client2 (pl: sKey, sec: sKey) = + let xored = xor(sec, pl) in + out (cs, (xored)). + + +query attacker(plain1). +query attacker(plain2). + +(* + * ============== + * Run the verification + * ============== + *) + + +process + (!client1(plain1, secret)) | (!client2(plain2, secret)) + + + +