Question about Modeling ECIES_MAC in Tamarin

[何子林]

Hi，

In my protocol, one step is designed as follows: The sender, following the ECIES scheme, utilizes the recipient's public key to generate encrypted transmission data comprising three components: 1) the sender's ephemeral public key, denoted as C0; 2) the data C1, which is encrypted using the symmetric encryption key K1 derived from the ECIES shared secret; and 3) the message authentication code (MAC) C2 for C1, generated using the MAC key K2 derived from the same ECIES shared secret. The sender then transmits the tuple <C0, C1, C2>along with Sig_t(a signature generated using the sender's private key over the hash of the entire transmission data) to a public channel.

Concurrently, upon receiving the structure <<C0, C1, C2>, Sig_t>, the recipient executes the state transition rule keypod_encryption.

During the ECIES decryption phase on the recipient's side, my state transition rule keypod_encryptionimposes two Eq( )constraints: 1) verifying the validity of the sender's signature Sig_ton the hash of the communication data using the recipient's computed hash; and 2) ensuring the computed MAC by the recipient matches the received MAC C2. Logically, if constraint 1 is satisfied (which guarantees the integrity of alltransmitted data), constraint 2 should inherently hold, as the MAC verification is a subset of the overall data integrity checked by the signature.

However, I am currently facing a formal verification issue: When I include only constraint 1 in the relevant state transition rule, the existence lemma is proven successfully.But when I add both constraint 1 and constraint 2 simultaneously, the existence lemma in my theory fails to prove. The failed proof trace indicates that an In( )on the left-hand side of the rule does not match the expected Out( )on the trace. Does anyone know how to fix this, or where the problem might originate from? 

Here is an excerpt of the theory.

functions: pk/1, sign/2, verify/3, h/1, senc/2, sdec/2,
//ECIES (https://www.usenix.org/system/files/sec21-wang-yuchen.pdf)
encap/2, getkey/1, getcipher/1, decap/2,
parse1/1, parse2/1, mac/2
equations:
    verify(sign(m, sk), m, pk(sk)) = true,
    decap(sk, getcipher(encap(pk(sk), r))) = getkey(encap(pk(sk), r))

rule app_encryption:
    let
       
na = p_na
nb = p_nb
auth_status = p_auth_status
Sig_b = p_Sig_b
Sig_t = p_Sig_t

        result_encap = encap(KPPublicKey, ~APP_esk)
        cipher = getcipher(result_encap)//Sender's ephemeral public key
        key = getkey(result_encap)//Shared key

        k1 = parse1(key)
        k2 = parse2(key)

        C1 = senc(data, k1)
        C2 = mac(C1, k2)

        senct = <cipher, C1, C2>
        hash = h(<na, Bind_Tuple, nb, Sig_b, senct>)
        Sig_t = sign(hash, UserPrivateKey)

    in
    [
        F_State_A2($User,$Keypod1, p_na,p_nb,p_auth_status,p_Sig_b,p_Sig_t ),
        Fr(~APP_esk),
        !PkK($Keypod1, KPPublicKey),
        !Data($User, data),
        !Bind($Keypod1, $Keypod2, $Keypod3, $User, $RegCenter, Bind_Tuple),
        !LtkU($User, UserPrivateKey)
    ]
    --[ AppEnc($User, $Keypod1, $RegCenter, data) ]->
    [
        F_State_A3($User,$Keypod1, na,nb,auth_status,Sig_b,Sig_t ),
        Out(<senct, Sig_t, '3'>)
    ]

rule keypod_decryption:
    let
       
na = p_na
nb = p_nb
auth_status = p_auth_status
Sig_b = p_Sig_b
Sig_t = p_Sig_t

        auth_status = <'0', 'auth'>

        senct = <C0, C1, C2>
        hash = h(<na, Bind_Tuple, nb, Sig_b, senct>)
        Sig_t = SignatureT
        result_Sig_t = verify(Sig_t, hash, UserPublicKey)

        key = decap(C0, KPPrivateKey)
        k1 = parse1(key)
        k2 = parse2(key)
        mac = mac(C1, k2)
        data = sdec(C1, k1)
    in
    [
        F_State_K2($Keypod1,$User,$RegCenter, p_na,p_nb,p_auth_status,p_Sig_b,p_Sig_t ),
        In(<<C0, C1, C2>, SignatureT, '3'>),
        !LtkK($Keypod1, KPPrivateKey),
        !Bind($Keypod1, $Keypod2, $Keypod3, $User, $RegCenter, Bind_Tuple),
        !PkU($User, UserPublicKey)
    ]
    --[ Eq(mac, C2),
        Eq(result_Sig_t, true),          
        CIdentity($Keypod1, $User, $RegCenter, <'0', 'auth'>),
        CNonces($Keypod1, $User, $RegCenter, <na, nb>),
        DataBackup($Keypod1, $User, $RegCenter, data) ]->
    [
        F_State_K3($Keypod1,$User,$RegCenter, na,nb,auth_status,Sig_b,Sig_t ),
        !Data_Backup($Keypod1, $User, $RegCenter, data)
    ]

lemma data_backup_honest_setup:
    exists-trace
    " Ex Keypod User RegCenter data #i.
        DataBackup(Keypod, User, RegCenter, data) @ i
        & not (Ex #r. LtkKReveal(Keypod) @ r & #r < #i)
        & not (Ex #r. LtkUReveal(User) @ r & #r < #i)
        & not (Ex #r. LtkRReveal(RegCenter) @ r & #r < #i)
        & not (Ex #r. DataReveal(User) @ r & #r < #i)
    "

Meanwhile, I am attaching two proof trace graphs provided by Tamarin：

contraint 1 only (trace found). Constraint 1 and 2 both （contradiction）

Thanks in advance，

Hezl

[Felix Linker]

Hi Hezl,

You ask a very involved question about detailed aspects of a complex protocol. It is not easy to tell you why Tamarin does not find a trace - beyond the obvious that there is no trace satisfying all your restrictions. I glanced at your model and could not see any obvious flaw.

I fear you must debug your model like you would a program. For example, you could delete components that should be unrelated to the bug, and hopefully you will find the modelling flaw.

Sorry to not be of better help. I hope you find the issue!

Best,

Felix

--
You received this message because you are subscribed to the Google Groups "Tamarin-prover" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tamarin-prove...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tamarin-prover/298f2b20-96c5-4e3f-9ba1-8a059264e6c5n%40googlegroups.com.