Un protocole randomisé utilise l`assignation aléatoire, par exemple le lancer de pièces électroniques, et sa terminaison est donc probabiliste. Les exigences relatives à un protocole d`accord randomisé sont les suivantes: en plus de la validité et de l`accord, le protocole garantit la résiliation probabiliste dans le temps attendu constant qui est validé par le biais de la propriété suivante: plus de détails sur la cadence SMV code et les preuves de validité, accord et convergence rapide peuvent être trouvées ici. Il convient de souligner que nous ne pouvons pas automatiser l`argument inductif final tel qu`il est probabiliste: cadence SMV ne peut pas gérer les probabilités, alors que PRISM ne peut gérer que des configurations finies et ne prend pas en charge la réduction des données. Au lieu de cela, nous validons également l`analyse probabiliste comme suit. En observant que, pour un n fixe, le problème peut être réduit au modèle vérifiant une abstraction finie d`État du protocole, nous construisons manuellement une abstraction et le modèle vérifient à l`aide de PRISM, validant les probabilités pour jusqu`à n = 20 parties. En outre, nous vérifions (pour une configuration finie) l`exactitude de l`abstraction à l`aide de l`algèbre de processus CSP [Ros97] et de l`outil FDR basé sur la méthode dans [KNS01a]; Cela dépend de la capacité à coder les probabilités dans les noms d`action, et empêche donc l`utilisation de cadence SMV. Nous surmonterons les défis ci-dessus comme suit. Nous modélisons le protocole complet dans cadence SMV, après avoir remplacé les résultats aléatoires par des choix non déterministes. Les difficultés techniques mentionnées avec le type de données ordset ont été résolues en grande partie par la recherche d`une variante du modèle qui préserve la propriété de clé sur laquelle repose l`argument de l`exactitude.
La preuve de la propriété probabiliste se réduit ensuite à un argument inductif simple et de haut niveau basé sur un certain nombre de lemmes et d`hypothèses cryptographiques. Nous assumons les propriétés cryptographiques et automatisons la preuve de chaque lemme. Ensemble avec les preuves de validité et d`accord, qui sont plus simples et entièrement automatisés, nous obtenons un argument partiellement mécanisé pour l`exactitude du protocole ABBA pour tous les n et pour tous les tours. L`objectif est d`automatiser l`analyse du protocole ABBA en utilisant la méthodologie introduite dans notre article antérieur [KNS01a] sur la base de [MQS00]. Dans [KNS01a], nous avons utilisé cadence SMV et le vérificateur de modèle probabiliste PRISM pour vérifier le protocole d`accord randomisé plus simple d`Aspnes et Herlihy [AH90] qui tolère uniquement les échecs d`arrêt bénins. Nous l`avons obtenue grâce à une combinaison de preuves mécaniques inductives (pour tous les n pour les propriétés non probabilistes) et de contrôles (pour les configurations finies en cas de propriétés probabilistes) plus une preuve manuelle de haut niveau. Le protocole ABBA, cependant, nous a présenté un certain nombre de difficultés non rencontrées plus tôt: un certain nombre de solutions au protocole de l`accord byzantin existent. Malheureusement, le résultat de l`impossibilité fondamentale de [FLP85] démontre qu`il n`existe aucun algorithme déterministe pour parvenir à un accord dans le cadre asynchrone, même contre les défaillances bénignes. Une solution qui surpasse ce problème, introduite pour la première fois par Rabin [Rab83] et Ben-or [Ben83], est d`utiliser la randomisation. Les primitives cryptographiques utilisées par le protocole sont des schémas de jetons d`accès aléatoire au seuil et des schémas de signature de seuil non interactifs qui, pour cette étude de cas, nous présumons être sécurisés.
En particulier, nous supposons que les systèmes de jetons à accès aléatoire de seuil sont robustes et imprévisibles, et que les schémas de signature de seuil sont robustes et non forgeables (voir [CKS00] pour plus de détails). Nous considérons le protocole d`accord byzantin randomisé ABBA (accord asynchrone binaire byzantin) de Cachin, Kursawe et Shoup [CKS00] qui est placé dans un environnement complètement asynchrone, permet le nombre maximal de parties corrompues et fait usage de la cryptographie et la randomisation. Il y a n parties, un adversaire qui est autorisé à corrompre au plus t d`entre eux (où t < n/3), et un concessionnaire de confiance. Les parties procèdent peut-être à de nombreux rounds: à chaque tour, elles tentent de se mettre d`accord en lançant des votes sur la base des votes d`autres parties.
