Re: [Rats] Follow-up CoRIM: Horn clauses

[Muhammad Usama Sardar <[e-mail]>]

None of the two issues pointed below mention Horn clauses. Also, the 
CoRIM meeting this week was cancelled. Some preliminary questions for 
better understanding:

  * How are "Horn clauses" relevant to the CoRIM draft? I don't fully
    understand the link of the CoRIM draft to Horn clauses.
  * How are the Horn clauses generated?
  * What are the assumptions/facts?
  * Which rule engine do you plan to use to analyze the Horn clauses?

We have some experience with Horn clauses, which will likely be helpful 
here, e.g., I have experience with ProVerif which is based on Horn 
clauses, and my colleagues have developed "Nemo" tool [1].

Since CoRIM is a WG document, could the editors and contributors please 
make a good-will effort to summarize the discussions on these meetings 
to the WG? Interested WG members would then get a chance to contribute 
and/or comment. This was already pointed out a couple of months ago [2], 
but I don't see any CoRIM update provided to the mailing list since 
then. I very much like the updates from PKIX attestation, e.g., [3].

[1] https://iccl.inf.tu-dresden.de/web/Inproceedings3354

[2] https://mailarchive.ietf.org/arch/msg/rats/OwTI-PfFpLXHKf3IhoNpayv3m10/

[3] https://mailarchive.ietf.org/arch/msg/rats/8X3N9e7-phCjDwGacWJrDoapeRE/

Thanks,

Usama

On 19.03.24 13:46, Yogesh Deshpande wrote:
> Hi Usama,
>
> Some of the linked github issues where the discussions happened is given below:
>
> https://github.com/ietf-rats-wg/draft-ietf-rats-corim/issues/197
>
> https://github.com/ietf-rats-wg/draft-ietf-rats-corim/issues/142
>
> Feel free to join CoRIM Meetings, I have forwarded you the invite.
>
> Regards,
> Yogesh
>
> -----Original Message-----
> From: Muhammad Usama Sardar<[e-mail]>
> Sent: Tuesday, March 19, 2024 12:05 PM
> To: Yogesh Deshpande<[e-mail]>
> Cc:[e-mail]
> Subject: Re: [Rats] Follow-up CoRIM: Horn clauses
>
> Hi Yogesh,
>
> Thanks. Could you point me to the recording and minutes of the relevant CoRIM team meeting where it was discussed?
>
> Usama
>
> On 19.03.24 12:53, Yogesh Deshpande wrote:
>> Hello Usama,
>>
>> This was only discussed recently in one of our CoRIM team meetings(has just been initiated), hence you do not find any update on the same in any of the IETF drafts.
>>
>> In the course of time, as part of CoRIM Verifier simplification
>> activity, concepts from this presentation will make its space into the draft.
>>
>> Regards,
>> Yogesh Deshpande
>>
>> -----Original Message-----
>> From: RATS<[e-mail]>  On Behalf Of Muhammad Usama Sardar
>> Sent: Tuesday, March 19, 2024 11:43 AM
>> To:[e-mail]
>> Subject: [Rats] Follow-up CoRIM: Horn clauses
>>
>> Dear Ned and CoRIM team,
>>
>> Horn clauses [1, slide 6] were mentioned yesterday in the meeting.
>> Surprisingly, I don't see any relevant discussion in any of the two relevant drafts [2,3]. Where can I find more details about how the Horn clauses are generated for any of these drafts? What are the assumptions/facts? etc.
>>
>> Thanks,
>>
>> Usama
>>
>> [1]
>> https://datatracker.ietf.org/meeting/119/materials/slides-119-rats-att
>> estation-verifier-theory-of-operation
>>
>> [2]https://datatracker.ietf.org/doc/draft-ietf-rats-corim/
>>
>> [3]
>> https://datatracker.ietf.org/doc/draft-cds-rats-intel-corim-profile/