Discussion :

[rmaker]

Messieurs dames, bonjour,

je cherche à savoir s'il existe une logique formelle pour la preuve de protocoles. En particulier, si on prend le cryptosystème d'El Gamal, on lit des éléments comme:

• Alice envoie à Bob de l'information (générateur d'un corps, cardinal de celui ci notamment)
• Alice génère de information (comme par exemple une puissance du dit générateur)
• Bob déduit telle information de ce qu'il sait
• etc

Donc, ma question est la suivante: pour prouver un cryptosystème, existe t'il une logique formelle qui distingue acteur et information, et qui modélise qu'un acteur sait, envoie, reçoit ou génère de l'information?
Est ce que ça parle à quelqu'un-e? Il y aurait dans cette logique plusieurs choses: prise en compte du temps, déduction d'une information par un acteur, impossibilité pour cet acteur de déduire autre chose, etc. Avez vous un lien? Une référence? Une piste?

Merci beaucoup cher forum, vous êtes formidables

[dahtah]

Salut,

Oui, ca existe et c'est fait pour la plupart des protocoles cryptographiques (recherche: el gamal formal verification, etc ...).

Par contre, si je comprends bien ta question, je ne crois pas s'il existe un standard ou une methode regissant la methode de verification en soit. Generallement, le papier pose les conditions d'attaque (threat model) et prouve en quoi le protocole est resistant.

Par exemple, la notion de

prise en compte du temps, déduction d'une information par un acteur, impossibilité pour cet acteur de déduire autre chose, etc

est le threat model defini dans le papier, mais il n'y a pas a ma connaissance de standard le regissant.
C'est d'ailleur en posant un threat model different que l'on trouve des attaques differentes.

Je sais pas si ca repond a ta question...

[rmaker]

Salut,

Oui, ca existe et c'est fait pour la plupart des protocoles cryptographiques (recherche: el gamal formal verification, etc ...).

Oui! Je connaissais, depuis peu. Les mathématiques derrière sont assez extraordinaires! Merci

Par contre, si je comprends bien ta question, je ne crois pas s'il existe un standard ou une methode regissant la methode de verification en soit. Generallement, le papier pose les conditions d'attaque (threat model) et prouve en quoi le protocole est resistant.

Par exemple, la notion de est le threat model defini dans le papier, mais il n'y a pas a ma connaissance de standard le regissant.
C'est d'ailleur en posant un threat model different que l'on trouve des attaques differentes.

Je sais pas si ca repond a ta question...

Déjà, merci pour ta réponse. C'est en effet la formalisation logique d'un threat model. Merci beaucoup