Resumen

Se proponen protocolos de firma de contrato multiparte optimistas (OMPCS) para intercambiar firmas digitales multiparte en un contrato. En comparación con los protocolos de intercambio de dos partes en general, tales protocolos son más complicados, ya que el número de mensajes y estados del protocolo aumenta considerablemente cuando aumentan los firmantes. Además, la propiedad de equidad en tales protocolos requiere protección de cada firmante en lugar de un agente hostil externo. Por lo tanto, presenta un desafío para la verificación formal. En nuestro análisis, empleamos y combinamos la fortaleza del lenguaje de modelado extendido CSP# y la lógica temporal lineal (LTL) para verificar la equidad de los protocolos OMPCS. Además, para resolver o mitigar el problema de explosión del espacio de estados, establecemos un algoritmo de reducción de estados que puede disminuir adecuadamente los estados redundantes y reducir enormemente la complejidad temporal y espacial. Finalmente, este documento ilustra la viabilidad de nuestro enfoque mediante el análisis de los protocolos GM y CKS

• Materias:Modelos matemáticos Conjuntos difusos Ecuaciones integrales Fusión de características Algoritmo de optimización
• Subjects:Mathematical models Fuzzy sets Integral equations Feature fusion Optimization algorithm
• Palabras claves:Propuesto; Firma de contrato multipartito; Protocolos; Equidad; Verificación formal; Algoritmo de reducción de estado
• Keywords:Proposed; Multiparty contract signing; Protocols; Fairness; Formal verification; State reduction algorithm