theory YubikeyHSM begin section{* The Yubikey-Protocol with a YubiHSM *} /* * Protocol: Yubikey Protocol with a YubiHSM * Modeler: Robert Kunnemann, Graham Steel * Date: August 2012 * * Status: working */ builtins: symmetric-encryption functions: S/1,zero/0 /* We to model the Yubikey protocol, described in * http://www.yubico.com/documentation * http://www.yubico.com/developers-intro * In this version, we assume the Authentication Server to be under the * control of the attacker. We investigate the secrecy of keys in case the * Authentication Server can protect the keys by encrypting them using a * Hardware Token called YubiHSM, see: * TODO URL will follow * This is simplified version, in particular: * - timestamps are not modelled * - we do not distinguish the session and token counter. We described them * as one single counter, that represents the pair (session counter, token * counter) with a lexicographical oder on the pair. * - we model encryption in more detail than the Theory Yubikey. However, * we use a very much simplified model of XOR * - we assume the YubiHSM to be in a configuration where only the flags * YSM_AEAD_RANDOM_GENERATE and * YSM_AEAD_YUBIKEY_OTP_DECODE * are activated. */ /* keystream models the way the keystream used for encryption is computed. * Mac describes the MAC used inside the AEADs, which are computed using * CBC mode, described in RFC 3610. * keystream_kh and keyhandle_n model the adversaries capacity to extract the * used keyhandle and nonce that determined the keystream. (Similar for * demac.) */ functions: keystream/2, keystream_kh/1, keystream_n/1, xorc/2, dexor1/2, dexor2/2, mac/2, demac/2 equations: keystream_kh(keystream(kh,n))=kh, keystream_n(keystream(n,n))=n, /* an incomplete way of modelling the algebraic properties of the XOR * operator */ dexor1(xorc(a,b),a)=b, dexor2(xorc(a,b),b)=a, /* using mac, adv might find out *something* about the message, we * overapproximate */ demac(mac(m,k),k)=m /* The following rules model two binary relations between integers. !Succ * is functional. If !Succ(a,b), then the adversary was able to show that b * is the successor of b. Similarly, albeit !Smaller is not functional, if * !Smaller(a,b), then the adversary was able to show that a is smaller * than b. * The Theory() action is used to enforce that this relation (to the extend * it is needed in this trace) has to be build up before running the first * protocol actions. */ rule InitSucc: [In(zero),In(S(zero))] --[Theory(), IsSucc(zero,S(zero)),IsZero(zero)]-> [!Succ(zero,S(zero))] rule StepSucc: [In(y),In(S(y)), !Succ(x,y)] --[Theory(), IsSucc(y,S(y)) ]-> [!Succ(y,S(y))] rule SimpleSmaller: [!Succ(x,y)] --[Theory(), IsSmaller(x,y)]-> [!Smaller(x,y)] rule ZExtendedSmaller: [!Smaller(x,y),!Succ(y,z)] --[Theory(), IsSmaller(x,z)]-> [!Smaller(x,z)] // Rules for intruder's control over Server /* The attacker can send messages to the HSM, i.e., on behalf of the * authentication server. Likewise, he can receive messages. */ rule isendHSM: [ In( x ) ] --[ HSMWrite(x) ]-> [ InHSM( x ) ] rule irecvHSM: [ OutHSM( x ) ] --[ HSMRead(x) ]-> [Out(x)] /* The attacker can write and read the Authentication Server's database. * This database contains a list of public ideas and corresponding AEADs */ rule read_AEAD: [ !S_AEAD(pid,aead) ] --[ AEADRead(aead),HSMRead(aead) ]-> [Out(aead)] rule write_AEAD: [ In(aead), In(pid) ] --[ AEADWrite(aead),HSMWrite(aead) ]-> [!S_AEAD(pid,aead) ] /* Initialisation of HSM and Authentication Server. OneTime() Assures that * this can only happen a single time in a trace */ rule HSMInit: [Fr(~k), Fr(~kh)] --[Protocol(), GenerateRole1(~k),MasterKey(~k), OneTime()]-> [ !HSM(~kh,~k), Out(~kh), /* If the following line is uncommented, we are able to reproduce the * attack described in * http://static.yubico.com/var/uploads/pdfs/Security%20Advisory.pdf */ //!YSM_AEAD_GENERATE(~kh), //uncomment to produce attacks !YSM_AEAD_YUBIKEY_OTP_DECODE(~kh) ] //Some commands on the HSM: rule YSM_AEAD_RANDOM_GENERATE: let ks=keystream(kh,N) aead= in [Fr(~data), InHSM(),!HSM(kh,k),!YSM_AEAD_RANDOM_GENERATE(kh)] --[GenerateRandomAEAD(~data)]-> [OutHSM( aead) ] rule YSM_AEAD_GENERATE: let ks=keystream(kh,N) aead= in [InHSM(),!HSM(kh,k),!YSM_AEAD_GENERATE(kh)] --[GenerateAEAD(data,aead )]-> [OutHSM( aead) ] rule YSM_AES_ESC_BLOCK_ENCRYPT: [InHSM(), !HSM(kh,k), !YSM_AES_ESC_BLOCK_ENCRYPT(kh)] --[]-> [OutHSM(senc(data,k))] rule YSM_AEAD_YUBIKEY_OTP_DECODE: let ks=keystream(kh,N) aead=),mac(,k)> otp=senc(,k2) in [InHSM(), !HSM(kh,k), !YSM_AEAD_YUBIKEY_OTP_DECODE(kh) ] --[ OtpDecode(k2,k,,sc,xorc(senc(ks,k),),mac(,k)), OtpDecodeMaster(k2,k) ]-> [OutHSM(sc)] //Yubikey operations //(see Yubikey.spthy for more detailed comments) rule BuyANewYubikey: let ks=keystream(kh,~pid) aead=),mac(<~k2,~sid>,~k)> in /* This rule implicitly uses YSM_AEAD_GENERATE to produce the AEAD that * stores the secret identity and shared key of a Yubikey. By disabling the * YSM_AEAD_GENERATE flag but nevertheless permitting this operation, we * model a scenario where YSM_AEAD_GENERATE can be safely used to guarantee * the operation, but not by the attacker. This corresponds to a scenario * where Yubikey set-up takes place on a different server, or where the * set-up takes place before the server is plugged into the network. * Uncomment the following line to require the HSM to have the * YSM_AEAD_GENERATE flag set. */ //!YSM_AEAD_GENERATE(kh), [ Fr(~k2),Fr(~pid),Fr(~sid), !HSM(kh,~k), !Succ(zero,one) ] --[Init(~pid,~k2)]-> [Y_counter(~pid,one), !Y_Key(~pid,~k2), !Y_sid(~pid,~sid), S_Counter(~pid,zero), !S_AEAD(~pid,aead), !S_sid(~pid,~sid), Out(~pid) ] //On plugin, the session counter is increased and the token counter reset rule Yubikey_Plugin: [Y_counter(pid,sc),!Smaller(sc, Ssc) ] //The old counter value sc is removed --[ Yubi(pid,Ssc) ]-> [Y_counter(pid, Ssc)] //and substituted by a new counter value, larger, Ssc rule Yubikey_PressButton: [Y_counter(pid,tc),!Y_Key(pid,k2),!Y_sid(pid,sid), !Succ(tc,Stc),Fr(~pr),Fr(~nonce) ] --[ YubiPress(pid,tc), YubiPressOtp(pid,,tc,k2) ]-> [Y_counter(pid,Stc), Out(,k2)>)] rule Server_ReceiveOTP_NewSession: let ks=keystream(kh,pid) aead=),mac(,k)> in [In(,k2)>) , !HSM(kh,k), !S_AEAD(pid,aead), S_Counter(pid,otc), !S_sid(pid,sid), !Smaller(otc,tc) ] --[ Login(pid,sid,tc,senc(,k2)), LoginCounter(pid,otc,tc) ]-> [ S_Counter(pid,tc) ] /* The following three axioms are conditions on the traces that make sure * that : */ // //a) the !Smaller relation is transitive axiom transitivity: //axiomatic "All #t1 #t2 a b c. IsSmaller(a,b)@t1 & IsSmaller(b,c)@t2 ==> Ex #t3 . IsSmaller(a,c)@t3 " //b) !Smaller implies unequality axiom smaller_implies_unequal: //axiomatic "not (Ex a #t . IsSmaller(a,a)@t)" /*c) The protocol runs only after the IsSmaller and IsSuccessor relation is * build up */ axiom theory_before_protocol: "All #i #j. Theory() @ i & Protocol() @ j ==> i < j" axiom onetime: "All #t3 #t4 . OneTime()@#t3 & OneTime()@t4 ==> #t3=#t4" //LEMMAS: // For sanity: Ensure that a successful login is reachable. //TODO reactivate //lemma Login_reachable: // exists-trace // "Ex #i pid sid x otp1. Login(pid,sid, x, otp1)@i" /* Every counter produced by a Yubikey could be computed by the adversary * anyway. (This saves a lot of steps in the backwards induction of the * following lemmas). */ lemma adv_can_guess_counter[reuse,use_induction]: "All pid sc #t2 . YubiPress(pid,sc)@t2 ==> (Ex #t1 . K(sc)@#t1 & #t1<#t2)" /* Everything that can be learned by using OtpDecode is the counter of a * Yubikey, which can be computed according to the previous lemma. */ lemma otp_decode_does_not_help_adv_use_induction[reuse,use_induction]: "All #t3 k2 k m sc enc mac . OtpDecode(k2,k,m,sc,enc,mac)@t3 ==> Ex #t1 pid . YubiPress(pid,sc)@#t1 & #t1<#t3" /* All keys shared between the YubiHSM and the Authentication Server are * either not known to the adversary, or the adversary learned the key used * to encrypt said keys in form of AEADs. */ lemma k2_is_secret_use_induction[use_induction,reuse]: "All #t1 #t2 pid k2 . Init(pid,k2)@t1 & K(k2)@t2 ==> (Ex #t3 #t4 k . K(k)@t3 & MasterKey(k)@t4 & #t3<#t2)" /* Neither of those kinds of keys are ever learned by the adversary */ lemma neither_k_nor_k2_are_ever_leaked_inv[use_induction,reuse]: " not( Ex #t1 #t2 k . MasterKey(k)@t1 & KU(k)@t2 ) & not (Ex #t5 #t6 k6 pid . Init(pid,k6)@t5 & KU(k6)@t6 ) " // Each succesful login with counter value x was preceeded by a PressButton // event with the same counter value // This lemma cannot be proven at the moment, but it would be a first step // to reach the no_replay result present in Yubikey.spthy lemma one_count_foreach_login[reuse,use_induction]: "All pid sid x otp #t2 . Login(pid,sid,x,otp)@t2 ==> ( Ex #t1 . YubiPress(pid,x)@#t1 & #t1<#t2 )" induction case empty_trace by contradiction // from formulas next case non_empty_trace simplify solve( !S_AEAD( pid, ), mac(, k)> ) ▶₂ #t2 ) case BuyANewYubikey_case_1 by sorry next case BuyANewYubikey_case_2 by sorry next case write_AEAD solve( !KU( xorc(senc(keystream(kh, pid), k), ) ) @ #vk.6 ) case irecv by contradiction // cyclic next case cxorc by sorry next case read_AEAD_case_1 by sorry next case read_AEAD_case_2 by sorry qed qed qed end