Tamarin Adversary knowledge

[Choro Ulan uulu]

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]

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.