A Framework for Analyzing Probabilistic Protocols and its Application to the Partial

Intend2

Description

Niveau: Supérieur, Doctorat, Bac+8
A Framework for Analyzing Probabilistic Protocols and its Application to the Partial Secrets Exchange ? Konstantinos Chatzikokolakis a, Catuscia Palamidessi a a INRIA Futurs and LIX, Ecole Polytechnique Abstract We propose a probabilistic variant of the pi-calculus as a framework to specify randomized security protocols and their intended properties. In order to express and verify the correctness of the protocols, we develop a probabilistic version of the testing semantics. We then illustrate these concepts on an extended example: the Partial Secret Exchange, a protocol which uses a randomized primitive, the Oblivious Transfer, to achieve fairness of information exchange between two parties. 1 Introduction Probabilistic security protocols involve probabilistic choices and are used for many purposes including signing contracts, sending certified email and pro- tecting the anonymity of communication agents. Some probabilistic protocols rely on specific random primitives such as the Oblivious Transfer ([14]). There are various examples in this category, notably the contract signing protocol in [6] and the privacy-preserving auction protocol in [9]. A large effort has been dedicated to the formal verification of security pro- tocols, and several approaches based on process-calculi techniques have been proposed. However, in the particular case of probabilistic protocols, they have been analyzed mainly by using model checking methods, while only few at- tempts of applying process calculi techniques have been made.

• pi calculus


• using probabilistic


• analyzing probabilistic


• oblivious transfer primitive


• probabilistic automata


• proto- col


• protocols


• exchange protocol


• transition group

Sujets

• École polytechnique
• Pi calculus
• Probabilistic automaton
• Protocol

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 27
• Langue: English

Extrait

Procédures

Procédure adaptée

Groupements commandes

Conformément à l'article 27 du code des marchés publics, ces marchés sont classés par catégories homogènes ou par unités fonctionnelles, pour les achats de fournitures et de services, et par opération pour les travaux, en fonction des procédures d'achat retenues.

Total

Autres procédures

ACADEMIE :NICE EXERCICE :2006

DATE : 06/03/06 PAGE :1

F118 - FRUITS ET LEGUMES FRAIS

F120 - LAIT-BEURRE

F119 - PREPARAT. ALIMENTAIRES ELABORE

5 916.18 5 011.04 744.83 1 038.12 1 488.82 2 864.33 6 118.47 5 834.15 7 629.60 6 162.47 1 489.66 21 237.15 569.70 3 434.55 3 143.90 4 178.43

Appels d'offres

Ce tableau fixe les montants en deçà desquels le chef d'établissement peut signer des marchés sans autorisation préalable du conseil d'administration,  enapplication de c) du 6°de l'article 16 du décret n°85924 du 30 août 1985 modifié.

 ETATPREVISIONNEL DE LA COMMANDE PUBLIQUE AU TITRE DE L'ANNEE 2006

0060033D LYCÉE D'ESTIENNED'ORVES NICE CEDEX 1

ETABLISSEMENT :

F115 - VOLAILLES PIECEES CONGELEES

F110 - VIANDE D'AGNEAU FRAICHE

Nomenclature(*) Fournitures F100 - LEGUMES SURGELES U CONGELES F101 - VIANDE SURGELEE OU CONGELEE F102 - CHARCUTERE SURGELEE OU CONGELE F104 - PRODUITS DE LA MER SURGELES F105 - AUTRES DESSERTS SURGELES OU CO

F109 - AUTRE VIANDE FAICHE

F108 - VIANDE DE VEAU FRAICHE

F107 - VIANDE DE BOEUF FRAICHE

F106 - AUTRES PRODUITS SURGELES OU CO

Article 30

Procédures négociées

Centrale d'achats

F111 - VIANDES ET ABATS DE PORC FRAIS

F114 - VOLAILLES ENTIERES

F113 - VOLAILLES

F112 - CHARCUTERIE

11 767.15 9 973.82 1 482.36 7 067.48 2 962.28 5 695.45 12 172.45 11 605.99 7 551.22 7 629.60 13 739.06 2 963.12 30 250.80 1 129.59 6 836.95 16 258.18 4 130.00 8 316.46

5 850.97 4 962.78 737.53 6 029.36 1 473.46 2 831.12 6 053.98 5 771.84 7 551.22 7 576.59 1 473.46 9 013.65 559.89 3 402.40 13 114.28 4 130.00 4 138.03