participate in it - Githubissues

huahuaLover commented 8 months ago

how to participate in this workshop? i am interested in it!

felixlinker commented 8 months ago

Hi! Glad to see that you're interested. Unfortunately, I don't know when I will host this workshop again. But two further notes:

I held this workshop one week ago at the IETF 118, and as part of that, it was recorded. You can find timestamps to the relevant parts of the recording here. This might help you with solving the exercises on your own :)
If you can think of any other occasion where you would like me to run the workshop, don't hesitate to reach out. You can find my contact details here.

huahuaLover commented 8 months ago

Thank you very much. If I expect you to host a workshop, I will get in touch with you！

felixlinker commented 8 months ago

There's no "right solution" to writing an oracle. I encourage you to watch my presentation from the IETF because in the second part, I go into the basic reasoning underlying manual proofs in Tamarin :) And writing an oracle is just an assisted way to prove a lemma manually.

If you have more, specific questions, I'd encourage you to post them to Tamarin's Google group. It is quite active!

huahuaLover commented 8 months ago

Thank you for your response.I am watching your presentation from the IETF :) As you mentioned, "writing an oracle is just an assisted way to prove a lemma manually," it means that we have manually proven the lemma first and then written the oracle. When we run it again, we use the pre-written oracle. Does it mean that the oracle is written based on our knowledge of how to prove a lemma?

huahuaLover commented 8 months ago

Thank you very much! I will post the specific questions to Tamarin's Google group.Thanks again!

felixlinker commented 8 months ago

As you mentioned, "writing an oracle is just an assisted way to prove a lemma manually," it means that we have manually proven the lemma first and then written the oracle.

No.

Does it mean that the oracle is written based on our knowledge of how to prove a lemma?

Yes! You don't need to prove the lemma completely first when writing an oracle. Partial proofs are fine. I always use an oracle of this form in my proofs: https://github.com/adem-wg/adem-proofs/blob/main/oracle.py (From a different project of mine.)

Documentation is not existent, but I think you can see what I'm going for :) I have a priority list of goals that I want to solve and I always solve the goal that matches the highest rank matcher.

huahuaLover commented 8 months ago

I am very sorry to take so long of your time. I am very grateful to receive your reply. I will continue to learn tamarin in the future

felixlinker commented 7 months ago

There is no recipe to follow. As I said, I suggest watching my presentation at the IETF. Beyond that, it's something that you must learn. I would not suggest looking at big projects like 5GAKA. These model real-world systems and are enormously complex. It's often better to look at small examples and understand how their proofs work. These projects need not have an oracle! You must first learn why proofs in Tamarin terminate.

huahuaLover commented 7 months ago

I am grateful to receive your response. I am watching your presentation at the IETF and have been working on ex3. I learned a lot from your presentation, and I truly appreciate it. I hope you can talk more about Tamarin-prover in the future because I noticed there are very few videos related to Tamarin-prover. As you mentioned, I will go ahead and study smaller examples. I plan to learn from the examples provided in Tamarin-prover.Do you have any suggestions for learning examples? Thank you so much

felixlinker commented 7 months ago

Hey! I cannot think of any specific models to look at, sorry :) I hope my exercises help.

huahuaLover commented 7 months ago

Thanks a lot!

felixlinker / tamarin-workshop

participate in it #4