Kvantinformationsbehandling, som är ett spännande forskningsområde i skärningspunkten mellan fysik och datavetenskap, har stor potential att påverka den framtida utvecklingen av informationsbehandlingssystem. Uppbyggandet av praktiska, allmänna ändamål Quantum Computers kan vara några år in i framtiden. Quantum Communication och Quantum Cryptography är dock väl utvecklade. Kommersiella Quantum Key Distribution system är lätt tillgängliga och flera QKD-nätverk har byggts i olika delar av världen. Säkerheten för de protokoll som används i dessa genomföranden bygger på informationsteoretiska bevis, som kan eller kanske inte återspeglar det faktiska systembeteendet. Dessutom kan testning av implementeringar inte garantera frånvaron av fel och fel. I detta dokument presenteras en ny ram för modellering och verifiering av kvantprotokoll och deras genomföranden med hjälp av bevisassistenten Coq. Vi tillhandahåller ett Coq-bibliotek för kvantbitar, kvantportar och kvantmätning. Som ett steg mot att verifiera praktiska kvantkommunikations- och säkerhetsprotokoll som Quantum Key Distribution stöder vi flera qubits, kommunikation och trassling. Vi illustrerar dessa begrepp genom att modellera Quantum Teleportation Protocol, som kommunicerar tillståndet för en okänd kvantbit med bara en klassisk kanal.
Boender m.fl. I Ref föreslogs en ram för att specificera och verifiera kvantprotokoll med hjälp av Coq.
Formalization of Quantum Protocols using Coq
{'venue': 'EPTCS 195, 2015, pp. 71-83', 'journal': None, 'mag_field_of_study': ['Computer Science']}