Tamarin Adversary knowledge

34 views
Skip to first unread message

Choro Ulan uulu

unread,
Aug 22, 2023, 9:20:58 AM8/22/23
to tamarin-prover

Hi,

 

I’m working on a university project where I’m trying to model symmetric encryption in tamarin. After I try to autoprove the adversary has somehow access to " challMsg  " even though I have never used Out() with this variable. It is only used with persistent and consumable facts. Here are some examples:

 

rule OracleChall:

  [ !OracleInit(challKey),

    PreChall(),

    Fr(~challMsg) ]

  -->

  [ RequestEncChall(challKey, ~challMsg) ]

 

rule EncryptionChall:

  [ RequestEncChall(challKey, challMsg), Fr(~ct),

    DecNotCalledYet()]

  -->

  [ !FactEncChall(challKey, challMsg, ~ct), Out(<'c', ~ct>) ]

 

!KU( ~challMsg ) @ #vk.2

 

How does the adversary get knowledge of "challMsg"?

 

Ralf Sasse

unread,
Aug 22, 2023, 10:58:44 AM8/22/23
to tamarin...@googlegroups.com, Choro Ulan uulu

With the information you are giving it looks to me that in interactive mode, you see a bubble with that KU(..) fact. However, it will not be connected to anything. This means that the adversary would need to know this. Thus, there will be a proof step available that tries to resolve said KU(...). Which, if it truly is underivable for the adversary, should fail, if resolved far enough back.

For more detailed suggestions we would need to see the actual input file.

Best regards,
Ralf

--
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 on the web visit https://groups.google.com/d/msgid/tamarin-prover/9ebd4e0a-ae15-461f-83f0-8ba3bae56088n%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages