# formule.ltl - controllato e corretto (si spera!)
#

# Unicita' della chiave
#
# usiamo i seguenti valori calcolati con cver:
#
# messaggio in chiaro 
#  m = 0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
# chiave 
#  k = 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
# messaggio cifrato
#  c = 1001100001000100010111111110010011001011101111010000010001110001011011010100010100010100011100010010011111001011010101100010110
#
G( (ready=1) -> ( ((m[127:0]=b0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)*(c[127:0]=b1001100001000100010111111110010011001011101111010000010001110001011011010100010100010100011100010010011111001011010101100010110)) -> !(k[127:0]=b1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000) ) );


# Ricerca della chiave
#
# usiamo le seguenti coppie della forma (messaggio in chiaro, messaggio cifrato) 
# calcolate con cver.
#
# prima coppia:
#  m = 0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
#  c = 1001100001000100010111111110010011001011101111010000010001110001011011010100010100010100011100010010011111001011010101100010110
# seconda coppia
#  m = 1111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111
#  c = 1001100011110001010101111010000100100101101111000100110101000111011011011110100100010100011100001010101110011001110000100010110
# terza coppia
#  m = 0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001
#  c = 1001100001000100010111111110010011001011101111010000010001110001011011010100010100010100011100010010011111001011010101100010110
#
# tutte le cifrature sono state eseguite con la seguente chiave
#  k = 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
#
# Neghiamo l'affermazione nella speranza di ottenere un controesempio;
# in questo modo dovremmo in teoria eseguire una crittoanalisi secondo 
# lo schema chosen plaintext.
#
! ( G ( (ready = 1) -> (( m[0:127] = 0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 * c[0:127] = 1001100001000100010111111110010011001011101111010000010001110001011011010100010100010100011100010010011111001011010101100010110 ) * ( m[0:127] = 1111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111 * c[0:127] = 1001100011110001010101111010000100100101101111000100110101000111011011011110100100010100011100001010101110011001110000100010110 ) * ( m[0:127] = 0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001 * c[0:127] = 1001100001000100010111111110010011001011101111010000010001110001011011010100010100010100011100010010011111001011010101100010110 ) )));