%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWV015+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Wed Jul 20 21:40:58 EDT 2022
% Result : Satisfiable 1.08s 1.24s
% Output : Saturation 1.08s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 1383)
% Comments :
%------------------------------------------------------------------------------
cnf(1384,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ intruder_message(generate_expiration_time(x))
| ~ intruder_message(u)
| ~ intruder_message(bt)
| ~ intruder_message(y)
| ~ party_of_protocol(y)
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(w)))
| ~ t_holds(key(bt,y))
| ~ t_holds(key(z,u))
| b_holds(key(generate_key(generate_b_nonce(w)),u)) ),
inference(mrr,[status(thm)],[1383,100]),
[iquote('0:MRR:1383.12,100.4')] ).
cnf(1391,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ a_nonce(w)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ party_of_protocol(y)
| ~ a_stored(pair(y,generate_b_nonce(v)))
| ~ a_stored(pair(b,w))
| ~ t_holds(key(generate_key(w),y))
| ~ t_holds(key(at,b))
| intruder_message(pair(encrypt(triple(b,generate_key(generate_b_nonce(v)),encrypt(triple(u,v,generate_expiration_time(v)),bt)),generate_key(w)),encrypt(x,generate_key(generate_b_nonce(v))))) ),
inference(res,[status(thm),theory(equality)],[1331,19]),
[iquote('0:Res:1331.14,19.0')] ).
cnf(1353,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ intruder_message(u)
| ~ intruder_message(bt)
| ~ intruder_message(x)
| ~ party_of_protocol(x)
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(w)))
| ~ t_holds(key(bt,x))
| ~ t_holds(key(y,u))
| b_holds(key(generate_key(generate_b_nonce(w)),u)) ),
inference(ssi,[status(thm)],[1347,7,145]),
[iquote('0:SSi:1347.10,1347.6,7.2,145.0,7.2,145.0')] ).
cnf(1395,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ party_of_protocol(y)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(generate_b_nonce(w)))
| ~ intruder_message(generate_expiration_time(x))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(w)))
| ~ intruder_holds(key(bt,y))
| b_holds(key(generate_key(generate_b_nonce(w)),u)) ),
inference(mrr,[status(thm)],[1394,100]),
[iquote('0:MRR:1394.11,100.4')] ).
cnf(1372,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ intruder_message(triple(u,generate_key(generate_b_nonce(w)),generate_expiration_time(x)))
| ~ party_of_protocol(y)
| ~ b_stored(pair(u,x))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(w)))
| ~ intruder_holds(key(bt,y))
| b_holds(key(generate_key(generate_b_nonce(w)),u)) ),
inference(sor,[status(thm)],[1341,33]),
[iquote('0:SoR:1341.5,33.3')] ).
cnf(1390,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ a_nonce(x)
| ~ intruder_message(x)
| ~ fresh_to_b(x)
| ~ intruder_message(y)
| ~ intruder_message(z)
| ~ a_nonce(v)
| ~ party_of_protocol(z)
| ~ a_stored(pair(z,v))
| ~ a_stored(pair(b,x))
| ~ t_holds(key(generate_key(x),z))
| ~ t_holds(key(at,w))
| intruder_message(pair(encrypt(triple(w,generate_key(v),u),generate_key(x)),encrypt(y,generate_key(v)))) ),
inference(res,[status(thm),theory(equality)],[1277,19]),
[iquote('0:Res:1277.14,19.0')] ).
cnf(1331,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ a_nonce(w)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ party_of_protocol(y)
| ~ a_stored(pair(y,generate_b_nonce(v)))
| ~ a_stored(pair(b,w))
| ~ t_holds(key(generate_key(w),y))
| ~ t_holds(key(at,b))
| message(sent(a,y,pair(encrypt(triple(b,generate_key(generate_b_nonce(v)),encrypt(triple(u,v,generate_expiration_time(v)),bt)),generate_key(w)),encrypt(x,generate_key(generate_b_nonce(v)))))) ),
inference(sor,[status(thm)],[123,1229]),
[iquote('0:SoR:123.0,1229.13')] ).
cnf(1382,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(generate_expiration_time(w))
| ~ intruder_message(bt)
| ~ intruder_message(x)
| ~ party_of_protocol(x)
| ~ b_stored(pair(b,w))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| ~ a_stored(pair(u,generate_b_nonce(v)))
| ~ t_holds(key(bt,x))
| b_holds(key(generate_key(generate_b_nonce(v)),b)) ),
inference(ssi,[status(thm)],[1364,7,145,2,111]),
[iquote('0:SSi:1364.11,1364.8,1364.0,7.0,145.0,7.2,145.0,2.2,111.0')] ).
cnf(1381,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(generate_expiration_time(w))
| ~ intruder_message(bt)
| ~ intruder_message(x)
| ~ party_of_protocol(x)
| ~ b_stored(pair(a,w))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| ~ a_stored(pair(u,generate_b_nonce(v)))
| ~ t_holds(key(bt,x))
| b_holds(key(generate_key(generate_b_nonce(v)),a)) ),
inference(ssi,[status(thm)],[1365,7,145,1,78]),
[iquote('0:SSi:1365.11,1365.8,1365.0,7.0,145.0,7.2,145.0,1.2,78.0')] ).
cnf(1251,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(generate_expiration_time(w))
| ~ intruder_message(u)
| ~ intruder_message(bt)
| ~ intruder_message(x)
| ~ party_of_protocol(x)
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(bt,x))
| ~ t_holds(key(y,u))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),u)) ),
inference(mrr,[status(thm)],[1250,100]),
[iquote('0:MRR:1250.10,100.4')] ).
cnf(1363,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ party_of_protocol(x)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(generate_b_nonce(w)))
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(w)))
| ~ intruder_holds(key(bt,x))
| b_holds(key(generate_key(generate_b_nonce(w)),u)) ),
inference(sor,[status(thm)],[1349,29]),
[iquote('0:SoR:1349.5,29.3')] ).
cnf(1277,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ a_nonce(x)
| ~ intruder_message(x)
| ~ fresh_to_b(x)
| ~ intruder_message(y)
| ~ intruder_message(z)
| ~ a_nonce(v)
| ~ party_of_protocol(z)
| ~ a_stored(pair(z,v))
| ~ a_stored(pair(b,x))
| ~ t_holds(key(generate_key(x),z))
| ~ t_holds(key(at,w))
| message(sent(a,z,pair(encrypt(triple(w,generate_key(v),u),generate_key(x)),encrypt(y,generate_key(v))))) ),
inference(sor,[status(thm)],[123,1208]),
[iquote('0:SoR:123.0,1208.13')] ).
cnf(1226,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ intruder_message(u)
| ~ intruder_message(bt)
| ~ intruder_message(w)
| ~ party_of_protocol(w)
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(bt,w))
| ~ t_holds(key(x,u))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),u)) ),
inference(ssi,[status(thm)],[1220,7,3,5,79,145]),
[iquote('0:SSi:1220.8,1220.4,7.0,3.0,5.0,79.2,145.0,3.0,5.0,79.0,7.0,3.0,5.0,79.2,145.0,3.0,5.0,79.0')] ).
cnf(1387,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ party_of_protocol(w)
| ~ a_stored(pair(w,generate_b_nonce(an_a_nonce)))
| ~ a_stored(pair(b,u))
| ~ t_holds(key(generate_key(u),w))
| ~ t_holds(key(at,b))
| intruder_message(pair(encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),generate_key(u)),encrypt(v,generate_key(generate_b_nonce(an_a_nonce))))) ),
inference(res,[status(thm),theory(equality)],[1306,19]),
[iquote('0:Res:1306.10,19.0')] ).
cnf(1292,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ a_nonce(y)
| ~ intruder_message(y)
| ~ fresh_to_b(y)
| ~ intruder_message(z)
| ~ a_nonce(w)
| ~ party_of_protocol(z)
| ~ a_stored(pair(z,w))
| ~ a_stored(pair(b,y))
| ~ t_holds(key(generate_key(y),z))
| ~ t_holds(key(at,x))
| message(sent(a,z,pair(u,encrypt(v,generate_key(w))))) ),
inference(con,[status(thm)],[1289]),
[iquote('0:Con:1289.2')] ).
cnf(1386,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(generate_b_nonce(w)))
| ~ intruder_message(generate_expiration_time(x))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(w)))
| b_holds(key(generate_key(generate_b_nonce(w)),u)) ),
inference(mrr,[status(thm)],[1385,100]),
[iquote('0:MRR:1385.11,100.4')] ).
cnf(1306,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ party_of_protocol(w)
| ~ a_stored(pair(w,generate_b_nonce(an_a_nonce)))
| ~ a_stored(pair(b,u))
| ~ t_holds(key(generate_key(u),w))
| ~ t_holds(key(at,b))
| message(sent(a,w,pair(encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),generate_key(u)),encrypt(v,generate_key(generate_b_nonce(an_a_nonce)))))) ),
inference(sor,[status(thm)],[123,1227]),
[iquote('0:SoR:123.0,1227.9')] ).
cnf(1371,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ intruder_message(triple(u,generate_key(generate_b_nonce(w)),generate_expiration_time(x)))
| ~ intruder_message(bt)
| ~ b_stored(pair(u,x))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(w)))
| b_holds(key(generate_key(generate_b_nonce(w)),u)) ),
inference(sor,[status(thm)],[1341,92]),
[iquote('0:SoR:1341.5,92.2')] ).
cnf(1362,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ a_nonce(x)
| ~ intruder_message(x)
| ~ fresh_to_b(x)
| ~ intruder_message(y)
| ~ party_of_protocol(y)
| ~ a_stored(pair(y,generate_b_nonce(w)))
| ~ a_stored(pair(b,x))
| ~ t_holds(key(generate_key(x),y))
| ~ t_holds(key(at,b))
| message(sent(a,y,pair(u,encrypt(v,generate_key(generate_b_nonce(w)))))) ),
inference(con,[status(thm)],[1359]),
[iquote('0:Con:1359.2')] ).
cnf(1341,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(encrypt(triple(u,generate_key(generate_b_nonce(w)),generate_expiration_time(x)),bt))
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ b_stored(pair(u,x))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(w)))
| b_holds(key(generate_key(generate_b_nonce(w)),u)) ),
inference(sor,[status(thm)],[1177,145]),
[iquote('0:SoR:1177.5,145.2')] ).
cnf(1349,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(triple(u,generate_key(generate_b_nonce(w)),generate_expiration_time(an_a_nonce)))
| ~ party_of_protocol(x)
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(w)))
| ~ intruder_holds(key(bt,x))
| b_holds(key(generate_key(generate_b_nonce(w)),u)) ),
inference(sor,[status(thm)],[1342,33]),
[iquote('0:SoR:1342.5,33.3')] ).
cnf(1338,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ fresh_to_b(w)
| ~ party_of_protocol(x)
| ~ t_holds(key(y,b))
| ~ t_holds(key(generate_key(v),u))
| ~ a_stored(pair(b,v))
| intruder_message(encrypt(quadruple(u,generate_b_nonce(w),generate_key(generate_b_nonce(w)),encrypt(triple(x,w,generate_expiration_time(w)),bt)),y)) ),
inference(con,[status(thm)],[1333]),
[iquote('0:Con:1333.2')] ).
cnf(1358,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ party_of_protocol(x)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(generate_b_nonce(an_a_nonce)))
| ~ intruder_message(generate_expiration_time(w))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| ~ intruder_holds(key(bt,x))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),u)) ),
inference(mrr,[status(thm)],[1357,100]),
[iquote('0:MRR:1357.9,100.4')] ).
cnf(1239,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(triple(u,generate_key(generate_b_nonce(an_a_nonce)),generate_expiration_time(w)))
| ~ party_of_protocol(x)
| ~ b_stored(pair(u,w))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| ~ intruder_holds(key(bt,x))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),u)) ),
inference(sor,[status(thm)],[1216,33]),
[iquote('0:SoR:1216.3,33.3')] ).
cnf(1356,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ a_nonce(w)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ party_of_protocol(y)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(w))
| ~ intruder_message(generate_expiration_time(x))
| ~ t_holds(key(bt,v))
| ~ a_stored(pair(v,w))
| ~ intruder_holds(key(bt,y))
| b_holds(key(generate_key(w),u)) ),
inference(mrr,[status(thm)],[1355,100]),
[iquote('0:MRR:1355.12,100.4')] ).
cnf(1354,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(generate_b_nonce(w)))
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(w)))
| b_holds(key(generate_key(generate_b_nonce(w)),u)) ),
inference(sor,[status(thm)],[1348,29]),
[iquote('0:SoR:1348.5,29.3')] ).
cnf(1010,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ a_nonce(w)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ intruder_message(triple(u,generate_key(w),generate_expiration_time(x)))
| ~ party_of_protocol(y)
| ~ b_stored(pair(u,x))
| ~ t_holds(key(bt,v))
| ~ a_stored(pair(v,w))
| ~ intruder_holds(key(bt,y))
| b_holds(key(generate_key(w),u)) ),
inference(sor,[status(thm)],[903,33]),
[iquote('0:SoR:903.6,33.3')] ).
cnf(1352,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ intruder_message(bt)
| ~ intruder_message(w)
| ~ party_of_protocol(w)
| ~ b_stored(pair(b,an_a_nonce))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| ~ a_stored(pair(u,generate_b_nonce(v)))
| ~ t_holds(key(bt,w))
| b_holds(key(generate_key(generate_b_nonce(v)),b)) ),
inference(ssi,[status(thm)],[1345,7,145,2,111]),
[iquote('0:SSi:1345.9,1345.6,1345.0,7.0,145.0,7.2,145.0,2.2,111.0')] ).
cnf(1348,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(triple(u,generate_key(generate_b_nonce(w)),generate_expiration_time(an_a_nonce)))
| ~ intruder_message(bt)
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(w)))
| b_holds(key(generate_key(generate_b_nonce(w)),u)) ),
inference(sor,[status(thm)],[1342,92]),
[iquote('0:SoR:1342.5,92.2')] ).
cnf(1351,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ intruder_message(bt)
| ~ intruder_message(w)
| ~ party_of_protocol(w)
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| ~ a_stored(pair(u,generate_b_nonce(v)))
| ~ t_holds(key(bt,w))
| b_holds(key(generate_key(generate_b_nonce(v)),a)) ),
inference(mrr,[status(thm)],[1350,88]),
[iquote('0:MRR:1350.8,88.0')] ).
cnf(1342,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(encrypt(triple(u,generate_key(generate_b_nonce(w)),generate_expiration_time(an_a_nonce)),bt))
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(w)))
| b_holds(key(generate_key(generate_b_nonce(w)),u)) ),
inference(sor,[status(thm)],[1177,112]),
[iquote('0:SoR:1177.5,112.0')] ).
cnf(1337,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ fresh_to_b(w)
| ~ party_of_protocol(x)
| ~ t_holds(key(y,b))
| ~ t_holds(key(generate_key(v),u))
| ~ a_stored(pair(b,v))
| intruder_message(encrypt(triple(b,generate_key(generate_b_nonce(w)),encrypt(triple(x,w,generate_expiration_time(w)),bt)),generate_key(v))) ),
inference(con,[status(thm)],[1334]),
[iquote('0:Con:1334.2')] ).
cnf(1177,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(generate_b_nonce(x))
| ~ intruder_message(encrypt(triple(u,generate_key(generate_b_nonce(w)),generate_expiration_time(x)),bt))
| ~ b_stored(pair(u,x))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(w)))
| b_holds(key(generate_key(generate_b_nonce(w)),u)) ),
inference(ssi,[status(thm)],[1176,8,7,145]),
[iquote('0:SSi:1176.1,8.2,7.0,145.0')] ).
cnf(1249,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ intruder_message(generate_expiration_time(v))
| ~ intruder_message(bt)
| ~ intruder_message(w)
| ~ party_of_protocol(w)
| ~ b_stored(pair(b,v))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| ~ a_stored(pair(u,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(bt,w))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),b)) ),
inference(ssi,[status(thm)],[1231,7,3,5,79,145,2,111]),
[iquote('0:SSi:1231.9,1231.6,1231.0,7.0,3.0,5.0,79.0,145.0,3.2,5.0,79.0,7.0,3.0,5.0,79.0,145.0,3.2,5.0,79.0,2.0,111.0')] ).
cnf(1248,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ intruder_message(generate_expiration_time(v))
| ~ intruder_message(bt)
| ~ intruder_message(w)
| ~ party_of_protocol(w)
| ~ b_stored(pair(a,v))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| ~ a_stored(pair(u,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(bt,w))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),a)) ),
inference(ssi,[status(thm)],[1232,7,3,5,79,145,1,78]),
[iquote('0:SSi:1232.9,1232.6,1232.0,7.0,3.0,5.0,79.0,145.0,3.2,5.0,79.0,7.0,3.0,5.0,79.0,145.0,3.2,5.0,79.0,1.0,78.0')] ).
cnf(1336,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ a_nonce(v)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ intruder_message(w)
| ~ party_of_protocol(w)
| ~ a_stored(pair(w,generate_b_nonce(u)))
| ~ a_stored(pair(b,v))
| ~ t_holds(key(generate_key(v),w))
| ~ t_holds(key(at,b))
| a_holds(key(generate_key(generate_b_nonce(u)),w)) ),
inference(con,[status(thm)],[1332]),
[iquote('0:Con:1332.0')] ).
cnf(1229,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ a_nonce(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ fresh_to_b(x)
| ~ party_of_protocol(y)
| ~ t_holds(key(z,b))
| ~ t_holds(key(generate_key(w),u))
| ~ a_stored(pair(b,w))
| intruder_message(triple(encrypt(quadruple(u,generate_b_nonce(x),generate_key(generate_b_nonce(x)),encrypt(triple(y,x,generate_expiration_time(x)),bt)),z),encrypt(triple(b,generate_key(generate_b_nonce(x)),encrypt(triple(y,x,generate_expiration_time(x)),bt)),generate_key(w)),v)) ),
inference(res,[status(thm),theory(equality)],[1110,19]),
[iquote('0:Res:1110.13,19.0')] ).
cnf(1318,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ a_nonce(w)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(x)
| ~ party_of_protocol(x)
| ~ a_stored(pair(x,generate_b_nonce(an_a_nonce)))
| ~ a_stored(pair(b,w))
| ~ t_holds(key(generate_key(w),x))
| ~ t_holds(key(at,b))
| message(sent(a,x,pair(u,encrypt(v,generate_key(generate_b_nonce(an_a_nonce)))))) ),
inference(sor,[status(thm)],[137,1313]),
[iquote('0:SoR:137.0,1313.8')] ).
cnf(1313,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ t_holds(key(w,b))
| ~ t_holds(key(generate_key(v),u))
| ~ a_stored(pair(b,v))
| intruder_message(encrypt(quadruple(u,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),w)) ),
inference(con,[status(thm)],[1308]),
[iquote('0:Con:1308.2')] ).
cnf(1312,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ t_holds(key(w,b))
| ~ t_holds(key(generate_key(v),u))
| ~ a_stored(pair(b,v))
| intruder_message(encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),generate_key(v))) ),
inference(con,[status(thm)],[1309]),
[iquote('0:Con:1309.2')] ).
cnf(1311,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ intruder_message(v)
| ~ party_of_protocol(v)
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| ~ a_stored(pair(b,u))
| ~ t_holds(key(generate_key(u),v))
| ~ t_holds(key(at,b))
| a_holds(key(generate_key(generate_b_nonce(an_a_nonce)),v)) ),
inference(con,[status(thm)],[1307]),
[iquote('0:Con:1307.3')] ).
cnf(1227,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ a_nonce(w)
| ~ t_holds(key(x,b))
| ~ t_holds(key(generate_key(w),u))
| ~ a_stored(pair(b,w))
| intruder_message(triple(encrypt(quadruple(u,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),x),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),generate_key(w)),v)) ),
inference(res,[status(thm),theory(equality)],[1109,19]),
[iquote('0:Res:1109.9,19.0')] ).
cnf(1263,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ a_nonce(x)
| ~ intruder_message(v)
| ~ intruder_message(y)
| ~ t_holds(key(generate_key(x),u))
| ~ a_stored(pair(b,x))
| ~ a_stored(pair(u,v))
| intruder_message(pair(encrypt(triple(a,generate_key(v),y),generate_key(x)),encrypt(w,generate_key(v)))) ),
inference(res,[status(thm),theory(equality)],[1215,19]),
[iquote('0:Res:1215.12,19.0')] ).
cnf(951,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ a_nonce(w)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ party_of_protocol(x)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(w))
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(bt,v))
| ~ a_stored(pair(v,w))
| ~ intruder_holds(key(bt,x))
| b_holds(key(generate_key(w),u)) ),
inference(sor,[status(thm)],[913,29]),
[iquote('0:SoR:913.6,29.3')] ).
cnf(1283,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ a_nonce(w)
| ~ intruder_message(x)
| ~ intruder_message(v)
| ~ intruder_message(y)
| ~ t_holds(key(z,x))
| ~ t_holds(key(generate_key(w),u))
| ~ a_stored(pair(b,w))
| intruder_message(encrypt(quadruple(u,v,generate_key(v),y),z)) ),
inference(con,[status(thm)],[1279]),
[iquote('0:Con:1279.3')] ).
cnf(1282,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ a_nonce(w)
| ~ intruder_message(x)
| ~ intruder_message(v)
| ~ intruder_message(y)
| ~ t_holds(key(z,x))
| ~ t_holds(key(generate_key(w),u))
| ~ a_stored(pair(b,w))
| intruder_message(encrypt(triple(x,generate_key(v),y),generate_key(w))) ),
inference(con,[status(thm)],[1280]),
[iquote('0:Con:1280.3')] ).
cnf(1208,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ a_nonce(x)
| ~ intruder_message(y)
| ~ intruder_message(v)
| ~ intruder_message(z)
| ~ t_holds(key(x1,y))
| ~ t_holds(key(generate_key(x),u))
| ~ a_stored(pair(b,x))
| intruder_message(triple(encrypt(quadruple(u,v,generate_key(v),z),x1),encrypt(triple(y,generate_key(v),z),generate_key(x)),w)) ),
inference(res,[status(thm),theory(equality)],[1108,19]),
[iquote('0:Res:1108.13,19.0')] ).
cnf(1265,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ party_of_protocol(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(generate_key(generate_b_nonce(u)))
| ~ intruder_message(generate_expiration_time(w))
| ~ a_stored(pair(b,generate_b_nonce(u)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ b_stored(pair(a,w))
| ~ intruder_holds(key(bt,v))
| b_holds(key(generate_key(generate_b_nonce(u)),a)) ),
inference(ssi,[status(thm)],[1264,1,78]),
[iquote('0:SSi:1264.5,1.0,78.0')] ).
cnf(1252,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ intruder_message(triple(a,generate_key(generate_b_nonce(u)),generate_expiration_time(v)))
| ~ party_of_protocol(w)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_stored(pair(b,generate_b_nonce(u)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ b_stored(pair(a,v))
| ~ intruder_holds(key(bt,w))
| b_holds(key(generate_key(generate_b_nonce(u)),a)) ),
inference(sor,[status(thm)],[1193,145]),
[iquote('0:SoR:1193.0,145.2')] ).
cnf(1230,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(generate_b_nonce(an_a_nonce)))
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| ~ intruder_holds(key(bt,w))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),u)) ),
inference(sor,[status(thm)],[1222,29]),
[iquote('0:SoR:1222.3,29.3')] ).
cnf(1262,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ a_nonce(w)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(w))
| ~ intruder_message(generate_expiration_time(x))
| ~ t_holds(key(bt,v))
| ~ a_stored(pair(v,w))
| b_holds(key(generate_key(w),u)) ),
inference(mrr,[status(thm)],[1261,100]),
[iquote('0:MRR:1261.12,100.4')] ).
cnf(1215,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ a_nonce(x)
| ~ intruder_message(v)
| ~ intruder_message(y)
| ~ t_holds(key(generate_key(x),u))
| ~ a_stored(pair(b,x))
| ~ a_stored(pair(u,v))
| message(sent(a,u,pair(encrypt(triple(a,generate_key(v),y),generate_key(x)),encrypt(w,generate_key(v))))) ),
inference(mrr,[status(thm)],[1214,12]),
[iquote('0:MRR:1214.9,12.0')] ).
cnf(1009,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ a_nonce(w)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ intruder_message(triple(u,generate_key(w),generate_expiration_time(x)))
| ~ intruder_message(bt)
| ~ b_stored(pair(u,x))
| ~ t_holds(key(bt,v))
| ~ a_stored(pair(v,w))
| b_holds(key(generate_key(w),u)) ),
inference(sor,[status(thm)],[903,92]),
[iquote('0:SoR:903.6,92.2')] ).
cnf(1260,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(generate_b_nonce(an_a_nonce)))
| ~ intruder_message(generate_expiration_time(w))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),u)) ),
inference(mrr,[status(thm)],[1259,100]),
[iquote('0:MRR:1259.9,100.4')] ).
cnf(1238,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(triple(u,generate_key(generate_b_nonce(an_a_nonce)),generate_expiration_time(w)))
| ~ intruder_message(bt)
| ~ b_stored(pair(u,w))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),u)) ),
inference(sor,[status(thm)],[1216,92]),
[iquote('0:SoR:1216.3,92.2')] ).
cnf(1256,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ party_of_protocol(v)
| ~ intruder_message(generate_key(generate_b_nonce(u)))
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ a_stored(pair(b,generate_b_nonce(u)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ intruder_holds(key(bt,v))
| b_holds(key(generate_key(generate_b_nonce(u)),a)) ),
inference(ssi,[status(thm)],[1255,1,78]),
[iquote('0:SSi:1255.3,1.0,78.0')] ).
cnf(1201,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ party_of_protocol(x)
| ~ a_stored(pair(x,generate_b_nonce(v)))
| ~ t_holds(key(generate_key(an_a_nonce),x))
| ~ t_holds(key(at,b))
| intruder_message(pair(encrypt(triple(b,generate_key(generate_b_nonce(v)),encrypt(triple(u,v,generate_expiration_time(v)),bt)),generate_key(an_a_nonce)),encrypt(w,generate_key(generate_b_nonce(v))))) ),
inference(res,[status(thm),theory(equality)],[1145,19]),
[iquote('0:Res:1145.10,19.0')] ).
cnf(1254,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ intruder_message(triple(a,generate_key(generate_b_nonce(u)),generate_expiration_time(an_a_nonce)))
| ~ party_of_protocol(v)
| ~ a_stored(pair(b,generate_b_nonce(u)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ intruder_holds(key(bt,v))
| b_holds(key(generate_key(generate_b_nonce(u)),a)) ),
inference(mrr,[status(thm)],[1253,88]),
[iquote('0:MRR:1253.7,88.0')] ).
cnf(1193,plain,
( ~ intruder_message(generate_b_nonce(u))
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ intruder_message(triple(a,generate_key(generate_b_nonce(v)),generate_expiration_time(u)))
| ~ party_of_protocol(w)
| ~ a_stored(pair(b,generate_b_nonce(v)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ b_stored(pair(a,u))
| ~ intruder_holds(key(bt,w))
| b_holds(key(generate_key(generate_b_nonce(v)),a)) ),
inference(sor,[status(thm)],[1172,33]),
[iquote('0:SoR:1172.0,33.3')] ).
cnf(1216,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(encrypt(triple(u,generate_key(generate_b_nonce(an_a_nonce)),generate_expiration_time(w)),bt))
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ b_stored(pair(u,w))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),u)) ),
inference(sor,[status(thm)],[1121,145]),
[iquote('0:SoR:1121.3,145.2')] ).
cnf(1222,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(triple(u,generate_key(generate_b_nonce(an_a_nonce)),generate_expiration_time(an_a_nonce)))
| ~ party_of_protocol(w)
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| ~ intruder_holds(key(bt,w))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),u)) ),
inference(sor,[status(thm)],[1217,33]),
[iquote('0:SoR:1217.3,33.3')] ).
cnf(1110,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ a_nonce(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ fresh_to_b(x)
| ~ party_of_protocol(y)
| ~ t_holds(key(z,b))
| ~ t_holds(key(generate_key(w),u))
| ~ a_stored(pair(b,w))
| message(sent(t,b,triple(encrypt(quadruple(u,generate_b_nonce(x),generate_key(generate_b_nonce(x)),encrypt(triple(y,x,generate_expiration_time(x)),bt)),z),encrypt(triple(b,generate_key(generate_b_nonce(x)),encrypt(triple(y,x,generate_expiration_time(x)),bt)),generate_key(w)),v))) ),
inference(ssi,[status(thm)],[1097,7,145]),
[iquote('0:SSi:1097.1,7.2,145.0')] ).
cnf(1228,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(generate_b_nonce(an_a_nonce)))
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),u)) ),
inference(sor,[status(thm)],[1221,29]),
[iquote('0:SoR:1221.3,29.3')] ).
cnf(1225,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ intruder_message(bt)
| ~ intruder_message(v)
| ~ party_of_protocol(v)
| ~ b_stored(pair(b,an_a_nonce))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| ~ a_stored(pair(u,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(bt,v))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),b)) ),
inference(ssi,[status(thm)],[1218,7,3,5,79,145,2,111]),
[iquote('0:SSi:1218.7,1218.4,1218.0,7.0,3.0,5.0,79.0,145.0,3.2,5.0,79.0,7.0,3.0,5.0,79.0,145.0,3.2,5.0,79.0,2.0,111.0')] ).
cnf(1221,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(triple(u,generate_key(generate_b_nonce(an_a_nonce)),generate_expiration_time(an_a_nonce)))
| ~ intruder_message(bt)
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),u)) ),
inference(sor,[status(thm)],[1217,92]),
[iquote('0:SoR:1217.3,92.2')] ).
cnf(1224,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ intruder_message(bt)
| ~ intruder_message(v)
| ~ party_of_protocol(v)
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| ~ a_stored(pair(u,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(bt,v))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),a)) ),
inference(mrr,[status(thm)],[1223,88]),
[iquote('0:MRR:1223.6,88.0')] ).
cnf(1109,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ a_nonce(w)
| ~ t_holds(key(x,b))
| ~ t_holds(key(generate_key(w),u))
| ~ a_stored(pair(b,w))
| message(sent(t,b,triple(encrypt(quadruple(u,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),x),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),generate_key(w)),v))) ),
inference(ssi,[status(thm)],[1098,7,3,5,79,145]),
[iquote('0:SSi:1098.1,7.0,3.0,5.0,79.2,145.0,3.0,5.0,79.0')] ).
cnf(1217,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(encrypt(triple(u,generate_key(generate_b_nonce(an_a_nonce)),generate_expiration_time(an_a_nonce)),bt))
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),u)) ),
inference(sor,[status(thm)],[1121,112]),
[iquote('0:SoR:1121.3,112.0')] ).
cnf(1121,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(v)
| ~ intruder_message(generate_b_nonce(w))
| ~ intruder_message(encrypt(triple(u,generate_key(generate_b_nonce(an_a_nonce)),generate_expiration_time(w)),bt))
| ~ b_stored(pair(u,w))
| ~ t_holds(key(at,b))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),u)) ),
inference(ssi,[status(thm)],[1120,8,7,3,5,79,145]),
[iquote('0:SSi:1120.1,8.0,7.0,3.0,5.2,79.0,145.0,3.0,5.0,79.0')] ).
cnf(1207,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ intruder_message(bt)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ intruder_message(generate_key(generate_b_nonce(u)))
| ~ intruder_message(generate_expiration_time(v))
| ~ a_stored(pair(b,generate_b_nonce(u)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ b_stored(pair(a,v))
| b_holds(key(generate_key(generate_b_nonce(u)),a)) ),
inference(ssi,[status(thm)],[1206,1,78]),
[iquote('0:SSi:1206.5,1.0,78.0')] ).
cnf(1213,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ a_nonce(w)
| ~ intruder_message(v)
| ~ t_holds(key(generate_key(w),u))
| ~ a_stored(pair(b,w))
| ~ a_stored(pair(u,v))
| a_holds(key(generate_key(v),u)) ),
inference(mrr,[status(thm)],[1212,12]),
[iquote('0:MRR:1212.7,12.0')] ).
cnf(1108,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ a_nonce(x)
| ~ intruder_message(y)
| ~ intruder_message(v)
| ~ intruder_message(z)
| ~ t_holds(key(x1,y))
| ~ t_holds(key(generate_key(x),u))
| ~ a_stored(pair(b,x))
| message(sent(t,y,triple(encrypt(quadruple(u,v,generate_key(v),z),x1),encrypt(triple(y,generate_key(v),z),generate_key(x)),w))) ),
inference(sor,[status(thm)],[431,29]),
[iquote('0:SoR:431.7,29.3')] ).
cnf(1196,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ intruder_message(triple(a,generate_key(generate_b_nonce(u)),generate_expiration_time(v)))
| ~ intruder_message(bt)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_stored(pair(b,generate_b_nonce(u)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ b_stored(pair(a,v))
| b_holds(key(generate_key(generate_b_nonce(u)),a)) ),
inference(sor,[status(thm)],[1192,145]),
[iquote('0:SoR:1192.0,145.2')] ).
cnf(1186,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ a_nonce(v)
| ~ party_of_protocol(y)
| ~ a_stored(pair(y,v))
| ~ t_holds(key(generate_key(an_a_nonce),y))
| ~ t_holds(key(at,w))
| intruder_message(pair(encrypt(triple(w,generate_key(v),u),generate_key(an_a_nonce)),encrypt(x,generate_key(v)))) ),
inference(res,[status(thm),theory(equality)],[1054,19]),
[iquote('0:Res:1054.10,19.0')] ).
cnf(1203,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ intruder_message(generate_key(generate_b_nonce(an_a_nonce)))
| ~ intruder_message(generate_expiration_time(v))
| ~ a_stored(pair(b,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ b_stored(pair(a,v))
| ~ intruder_holds(key(bt,u))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),a)) ),
inference(ssi,[status(thm)],[1202,1,78]),
[iquote('0:SSi:1202.3,1.0,78.0')] ).
cnf(1181,plain,
( ~ intruder_message(triple(a,generate_key(generate_b_nonce(an_a_nonce)),generate_expiration_time(u)))
| ~ party_of_protocol(v)
| ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ a_stored(pair(b,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ b_stored(pair(a,u))
| ~ intruder_holds(key(bt,v))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),a)) ),
inference(sor,[status(thm)],[1128,145]),
[iquote('0:SoR:1128.0,145.2')] ).
cnf(1145,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ party_of_protocol(x)
| ~ a_stored(pair(x,generate_b_nonce(v)))
| ~ t_holds(key(generate_key(an_a_nonce),x))
| ~ t_holds(key(at,b))
| message(sent(a,x,pair(encrypt(triple(b,generate_key(generate_b_nonce(v)),encrypt(triple(u,v,generate_expiration_time(v)),bt)),generate_key(an_a_nonce)),encrypt(w,generate_key(generate_b_nonce(v)))))) ),
inference(sor,[status(thm)],[123,1091]),
[iquote('0:SoR:123.0,1091.9')] ).
cnf(1200,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ intruder_message(bt)
| ~ intruder_message(generate_key(generate_b_nonce(u)))
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ a_stored(pair(b,generate_b_nonce(u)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| b_holds(key(generate_key(generate_b_nonce(u)),a)) ),
inference(ssi,[status(thm)],[1199,1,78]),
[iquote('0:SSi:1199.3,1.0,78.0')] ).
cnf(1198,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ intruder_message(triple(a,generate_key(generate_b_nonce(u)),generate_expiration_time(an_a_nonce)))
| ~ intruder_message(bt)
| ~ a_stored(pair(b,generate_b_nonce(u)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| b_holds(key(generate_key(generate_b_nonce(u)),a)) ),
inference(mrr,[status(thm)],[1197,88]),
[iquote('0:MRR:1197.7,88.0')] ).
cnf(1192,plain,
( ~ intruder_message(generate_b_nonce(u))
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ intruder_message(triple(a,generate_key(generate_b_nonce(v)),generate_expiration_time(u)))
| ~ intruder_message(bt)
| ~ a_stored(pair(b,generate_b_nonce(v)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ b_stored(pair(a,u))
| b_holds(key(generate_key(generate_b_nonce(v)),a)) ),
inference(sor,[status(thm)],[1172,92]),
[iquote('0:SoR:1172.0,92.2')] ).
cnf(1172,plain,
( ~ intruder_message(encrypt(triple(a,generate_key(generate_b_nonce(u)),generate_expiration_time(v)),bt))
| ~ intruder_message(generate_b_nonce(v))
| ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ a_stored(pair(b,generate_b_nonce(u)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ b_stored(pair(a,v))
| b_holds(key(generate_key(generate_b_nonce(u)),a)) ),
inference(ssi,[status(thm)],[1169,8,7,145,2,111]),
[iquote('0:SSi:1169.6,1169.5,1169.4,8.0,7.0,145.0,2.0,111.2,2.0,111.0')] ).
cnf(1054,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ a_nonce(v)
| ~ party_of_protocol(y)
| ~ a_stored(pair(y,v))
| ~ t_holds(key(generate_key(an_a_nonce),y))
| ~ t_holds(key(at,w))
| message(sent(a,y,pair(encrypt(triple(w,generate_key(v),u),generate_key(an_a_nonce)),encrypt(x,generate_key(v))))) ),
inference(sor,[status(thm)],[123,1033]),
[iquote('0:SoR:123.0,1033.9')] ).
cnf(1185,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(generate_key(generate_b_nonce(an_a_nonce)))
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ a_stored(pair(b,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ intruder_holds(key(bt,u))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),a)) ),
inference(ssi,[status(thm)],[1184,1,78]),
[iquote('0:SSi:1184.1,1.0,78.0')] ).
cnf(1183,plain,
( ~ intruder_message(triple(a,generate_key(generate_b_nonce(an_a_nonce)),generate_expiration_time(an_a_nonce)))
| ~ party_of_protocol(u)
| ~ a_stored(pair(b,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ intruder_holds(key(bt,u))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),a)) ),
inference(mrr,[status(thm)],[1182,88]),
[iquote('0:MRR:1182.5,88.0')] ).
cnf(1128,plain,
( ~ intruder_message(generate_b_nonce(u))
| ~ intruder_message(triple(a,generate_key(generate_b_nonce(an_a_nonce)),generate_expiration_time(u)))
| ~ party_of_protocol(v)
| ~ a_stored(pair(b,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ b_stored(pair(a,u))
| ~ intruder_holds(key(bt,v))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),a)) ),
inference(sor,[status(thm)],[1116,33]),
[iquote('0:SoR:1116.0,33.3')] ).
cnf(1178,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ party_of_protocol(v)
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ t_holds(key(at,b))
| intruder_message(pair(encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),generate_key(an_a_nonce)),encrypt(u,generate_key(generate_b_nonce(an_a_nonce))))) ),
inference(res,[status(thm),theory(equality)],[1081,19]),
[iquote('0:Res:1081.6,19.0')] ).
cnf(1081,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ party_of_protocol(v)
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ t_holds(key(at,b))
| message(sent(a,v,pair(encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),generate_key(an_a_nonce)),encrypt(u,generate_key(generate_b_nonce(an_a_nonce)))))) ),
inference(sor,[status(thm)],[123,1064]),
[iquote('0:SoR:123.0,1064.5')] ).
cnf(1170,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ party_of_protocol(x)
| ~ a_stored(pair(x,generate_b_nonce(w)))
| ~ t_holds(key(generate_key(an_a_nonce),x))
| ~ t_holds(key(at,b))
| intruder_message(pair(u,encrypt(v,generate_key(generate_b_nonce(w))))) ),
inference(res,[status(thm),theory(equality)],[1164,19]),
[iquote('0:Res:1164.9,19.0')] ).
cnf(1164,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ party_of_protocol(x)
| ~ a_stored(pair(x,generate_b_nonce(w)))
| ~ t_holds(key(generate_key(an_a_nonce),x))
| ~ t_holds(key(at,b))
| message(sent(a,x,pair(u,encrypt(v,generate_key(generate_b_nonce(w)))))) ),
inference(con,[status(thm)],[1159]),
[iquote('0:Con:1159.2')] ).
cnf(1166,plain,
( ~ intruder_message(bt)
| ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(generate_b_nonce(an_a_nonce)))
| ~ intruder_message(generate_expiration_time(u))
| ~ a_stored(pair(b,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ b_stored(pair(a,u))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),a)) ),
inference(ssi,[status(thm)],[1165,1,78]),
[iquote('0:SSi:1165.3,1.0,78.0')] ).
cnf(1131,plain,
( ~ intruder_message(triple(a,generate_key(generate_b_nonce(an_a_nonce)),generate_expiration_time(u)))
| ~ intruder_message(bt)
| ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ a_stored(pair(b,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ b_stored(pair(a,u))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),a)) ),
inference(sor,[status(thm)],[1127,145]),
[iquote('0:SoR:1127.0,145.2')] ).
cnf(1152,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(v)
| ~ party_of_protocol(w)
| ~ t_holds(key(x,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| intruder_message(encrypt(quadruple(u,generate_b_nonce(v),generate_key(generate_b_nonce(v)),encrypt(triple(w,v,generate_expiration_time(v)),bt)),x)) ),
inference(con,[status(thm)],[1147]),
[iquote('0:Con:1147.2')] ).
cnf(1151,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(v)
| ~ party_of_protocol(w)
| ~ t_holds(key(x,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| intruder_message(encrypt(triple(b,generate_key(generate_b_nonce(v)),encrypt(triple(w,v,generate_expiration_time(v)),bt)),generate_key(an_a_nonce))) ),
inference(con,[status(thm)],[1148]),
[iquote('0:Con:1148.2')] ).
cnf(1150,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ party_of_protocol(v)
| ~ a_stored(pair(v,generate_b_nonce(u)))
| ~ t_holds(key(generate_key(an_a_nonce),v))
| ~ t_holds(key(at,b))
| a_holds(key(generate_key(generate_b_nonce(u)),v)) ),
inference(con,[status(thm)],[1146]),
[iquote('0:Con:1146.0')] ).
cnf(1156,plain,
( ~ intruder_message(bt)
| ~ intruder_message(generate_key(generate_b_nonce(an_a_nonce)))
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ a_stored(pair(b,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),a)) ),
inference(ssi,[status(thm)],[1155,1,78]),
[iquote('0:SSi:1155.1,1.0,78.0')] ).
cnf(1133,plain,
( ~ intruder_message(triple(a,generate_key(generate_b_nonce(an_a_nonce)),generate_expiration_time(an_a_nonce)))
| ~ intruder_message(bt)
| ~ a_stored(pair(b,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),a)) ),
inference(mrr,[status(thm)],[1132,88]),
[iquote('0:MRR:1132.5,88.0')] ).
cnf(1091,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ fresh_to_b(w)
| ~ party_of_protocol(x)
| ~ t_holds(key(y,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| intruder_message(triple(encrypt(quadruple(u,generate_b_nonce(w),generate_key(generate_b_nonce(w)),encrypt(triple(x,w,generate_expiration_time(w)),bt)),y),encrypt(triple(b,generate_key(generate_b_nonce(w)),encrypt(triple(x,w,generate_expiration_time(w)),bt)),generate_key(an_a_nonce)),v)) ),
inference(res,[status(thm),theory(equality)],[902,19]),
[iquote('0:Res:902.9,19.0')] ).
cnf(1127,plain,
( ~ intruder_message(generate_b_nonce(u))
| ~ intruder_message(triple(a,generate_key(generate_b_nonce(an_a_nonce)),generate_expiration_time(u)))
| ~ intruder_message(bt)
| ~ a_stored(pair(b,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ b_stored(pair(a,u))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),a)) ),
inference(sor,[status(thm)],[1116,92]),
[iquote('0:SoR:1116.0,92.2')] ).
cnf(1116,plain,
( ~ intruder_message(encrypt(triple(a,generate_key(generate_b_nonce(an_a_nonce)),generate_expiration_time(u)),bt))
| ~ intruder_message(generate_b_nonce(u))
| ~ a_stored(pair(b,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),b))
| ~ t_holds(key(at,b))
| ~ b_stored(pair(a,u))
| b_holds(key(generate_key(generate_b_nonce(an_a_nonce)),a)) ),
inference(ssi,[status(thm)],[1113,8,7,3,5,79,145,2,111]),
[iquote('0:SSi:1113.4,1113.3,1113.2,8.0,7.0,3.0,5.0,79.0,145.0,3.0,5.2,79.0,2.0,111.0,2.0,111.0')] ).
cnf(1114,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ party_of_protocol(w)
| ~ a_stored(pair(w,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),w))
| ~ t_holds(key(at,b))
| intruder_message(pair(u,encrypt(v,generate_key(generate_b_nonce(an_a_nonce))))) ),
inference(res,[status(thm),theory(equality)],[1094,19]),
[iquote('0:Res:1094.7,19.0')] ).
cnf(1094,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ party_of_protocol(w)
| ~ a_stored(pair(w,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),w))
| ~ t_holds(key(at,b))
| message(sent(a,w,pair(u,encrypt(v,generate_key(generate_b_nonce(an_a_nonce)))))) ),
inference(sor,[status(thm)],[137,1088]),
[iquote('0:SoR:137.0,1088.4')] ).
cnf(431,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ a_nonce(x)
| ~ intruder_message(triple(y,v,z))
| ~ t_holds(key(x1,y))
| ~ t_holds(key(generate_key(x),u))
| ~ a_stored(pair(b,x))
| message(sent(t,y,triple(encrypt(quadruple(u,v,generate_key(v),z),x1),encrypt(triple(y,generate_key(v),z),generate_key(x)),w))) ),
inference(sor,[status(thm)],[150,429]),
[iquote('0:SoR:150.4,429.5')] ).
cnf(1096,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ party_of_protocol(v)
| ~ t_holds(key(w,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| ~ intruder_holds(key(w,v))
| intruder_message(w) ),
inference(res,[status(thm),theory(equality)],[1088,32]),
[iquote('0:Res:1088.4,32.1')] ).
cnf(1088,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ t_holds(key(v,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| intruder_message(encrypt(quadruple(u,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),v)) ),
inference(con,[status(thm)],[1083]),
[iquote('0:Con:1083.2')] ).
cnf(1087,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ t_holds(key(v,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| intruder_message(encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),generate_key(an_a_nonce))) ),
inference(con,[status(thm)],[1084]),
[iquote('0:Con:1084.2')] ).
cnf(1086,plain,
( ~ intruder_message(u)
| ~ party_of_protocol(u)
| ~ a_stored(pair(u,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| ~ t_holds(key(at,b))
| a_holds(key(generate_key(generate_b_nonce(an_a_nonce)),u)) ),
inference(con,[status(thm)],[1082]),
[iquote('0:Con:1082.0')] ).
cnf(902,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ fresh_to_b(w)
| ~ party_of_protocol(x)
| ~ t_holds(key(y,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| message(sent(t,b,triple(encrypt(quadruple(u,generate_b_nonce(w),generate_key(generate_b_nonce(w)),encrypt(triple(x,w,generate_expiration_time(w)),bt)),y),encrypt(triple(b,generate_key(generate_b_nonce(w)),encrypt(triple(x,w,generate_expiration_time(w)),bt)),generate_key(an_a_nonce)),v))) ),
inference(ssi,[status(thm)],[891,7,145]),
[iquote('0:SSi:891.1,7.2,145.0')] ).
cnf(1064,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ t_holds(key(w,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| intruder_message(triple(encrypt(quadruple(u,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),w),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),generate_key(an_a_nonce)),v)) ),
inference(res,[status(thm),theory(equality)],[901,19]),
[iquote('0:Res:901.5,19.0')] ).
cnf(1070,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ a_nonce(w)
| ~ party_of_protocol(y)
| ~ a_stored(pair(y,w))
| ~ t_holds(key(generate_key(an_a_nonce),y))
| ~ t_holds(key(at,x))
| message(sent(a,y,pair(u,encrypt(v,generate_key(w))))) ),
inference(con,[status(thm)],[1067]),
[iquote('0:Con:1067.2')] ).
cnf(1060,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(v)
| ~ intruder_message(x)
| ~ t_holds(key(y,w))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| intruder_message(encrypt(quadruple(u,v,generate_key(v),x),y)) ),
inference(con,[status(thm)],[1056]),
[iquote('0:Con:1056.3')] ).
cnf(1059,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(v)
| ~ intruder_message(x)
| ~ t_holds(key(y,w))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| intruder_message(encrypt(triple(w,generate_key(v),x),generate_key(an_a_nonce))) ),
inference(con,[status(thm)],[1057]),
[iquote('0:Con:1057.3')] ).
cnf(901,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ t_holds(key(w,b))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| message(sent(t,b,triple(encrypt(quadruple(u,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),w),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),generate_key(an_a_nonce)),v))) ),
inference(ssi,[status(thm)],[892,7,3,5,79,145]),
[iquote('0:SSi:892.1,7.0,3.0,5.0,79.2,145.0,3.0,5.0,79.0')] ).
cnf(1033,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(v)
| ~ intruder_message(y)
| ~ t_holds(key(z,x))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| intruder_message(triple(encrypt(quadruple(u,v,generate_key(v),y),z),encrypt(triple(x,generate_key(v),y),generate_key(an_a_nonce)),w)) ),
inference(res,[status(thm),theory(equality)],[900,19]),
[iquote('0:Res:900.9,19.0')] ).
cnf(1041,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(v)
| ~ intruder_message(x)
| ~ t_holds(key(generate_key(an_a_nonce),u))
| ~ a_stored(pair(u,v))
| intruder_message(pair(encrypt(triple(a,generate_key(v),x),generate_key(an_a_nonce)),encrypt(w,generate_key(v)))) ),
inference(res,[status(thm),theory(equality)],[1040,19]),
[iquote('0:Res:1040.8,19.0')] ).
cnf(1040,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(v)
| ~ intruder_message(x)
| ~ t_holds(key(generate_key(an_a_nonce),u))
| ~ a_stored(pair(u,v))
| message(sent(a,u,pair(encrypt(triple(a,generate_key(v),x),generate_key(an_a_nonce)),encrypt(w,generate_key(v))))) ),
inference(mrr,[status(thm)],[1039,12]),
[iquote('0:MRR:1039.6,12.0')] ).
cnf(1038,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ t_holds(key(generate_key(an_a_nonce),u))
| ~ a_stored(pair(u,v))
| a_holds(key(generate_key(v),u)) ),
inference(mrr,[status(thm)],[1037,12]),
[iquote('0:MRR:1037.4,12.0')] ).
cnf(900,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(v)
| ~ intruder_message(y)
| ~ t_holds(key(z,x))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| message(sent(t,x,triple(encrypt(quadruple(u,v,generate_key(v),y),z),encrypt(triple(x,generate_key(v),y),generate_key(an_a_nonce)),w))) ),
inference(sor,[status(thm)],[209,29]),
[iquote('0:SoR:209.4,29.3')] ).
cnf(1019,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ a_nonce(v)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(v)
| ~ party_of_protocol(w)
| ~ t_holds(key(bt,u))
| ~ a_stored(pair(u,v))
| ~ t_holds(key(x,w))
| b_holds(key(generate_key(v),w)) ),
inference(mrr,[status(thm)],[1018,100]),
[iquote('0:MRR:1018.7,100.4')] ).
cnf(1031,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ a_stored(pair(b,u))
| b_holds(key(generate_key(u),b)) ),
inference(ssi,[status(thm)],[1030,2,111]),
[iquote('0:SSi:1030.1,1030.0,2.0,111.0,2.0,111.0')] ).
cnf(1029,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ a_nonce(v)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ t_holds(key(bt,u))
| ~ a_stored(pair(u,v))
| b_holds(key(generate_key(v),b)) ),
inference(ssi,[status(thm)],[1028,2,111]),
[iquote('0:SSi:1028.1,1028.0,2.0,111.0,2.0,111.0')] ).
cnf(888,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(generate_expiration_time(v))
| ~ intruder_message(w)
| ~ intruder_message(u)
| ~ intruder_message(bt)
| ~ intruder_message(x)
| ~ a_nonce(w)
| ~ party_of_protocol(x)
| ~ intruder_message(generate_b_nonce(v))
| ~ party_of_protocol(y)
| ~ b_stored(pair(u,v))
| ~ t_holds(key(bt,x))
| ~ t_holds(key(z,u))
| ~ intruder_holds(key(generate_key(w),y))
| b_holds(key(generate_key(w),u)) ),
inference(sor,[status(thm)],[582,33]),
[iquote('0:SoR:582.1,33.3')] ).
cnf(903,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ a_nonce(w)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(encrypt(triple(u,generate_key(w),generate_expiration_time(x)),bt))
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ b_stored(pair(u,x))
| ~ t_holds(key(bt,v))
| ~ a_stored(pair(v,w))
| b_holds(key(generate_key(w),u)) ),
inference(sor,[status(thm)],[864,145]),
[iquote('0:SoR:864.6,145.2')] ).
cnf(998,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ a_nonce(w)
| ~ intruder_message(v)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(generate_expiration_time(x))
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ t_holds(key(at,u))
| ~ t_holds(key(bt,v))
| ~ a_stored(pair(v,w))
| b_holds(key(generate_key(w),u)) ),
inference(mrr,[status(thm)],[996,100]),
[iquote('0:MRR:996.10,100.4')] ).
cnf(997,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ a_nonce(w)
| ~ intruder_message(v)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(at,u))
| ~ t_holds(key(bt,v))
| ~ a_stored(pair(v,w))
| b_holds(key(generate_key(w),u)) ),
inference(sor,[status(thm)],[929,112]),
[iquote('0:SoR:929.4,112.0')] ).
cnf(929,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ a_nonce(w)
| ~ intruder_message(v)
| ~ intruder_message(generate_b_nonce(x))
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(generate_expiration_time(x))
| ~ b_stored(pair(u,x))
| ~ t_holds(key(at,u))
| ~ t_holds(key(bt,v))
| ~ a_stored(pair(v,w))
| b_holds(key(generate_key(w),u)) ),
inference(ssi,[status(thm)],[926,8]),
[iquote('0:SSi:926.1,8.0')] ).
cnf(875,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ party_of_protocol(y)
| ~ a_stored(pair(y,generate_b_nonce(v)))
| ~ t_holds(key(w,y))
| ~ t_holds(key(at,b))
| intruder_message(pair(encrypt(triple(b,generate_key(generate_b_nonce(v)),encrypt(triple(u,v,generate_expiration_time(v)),bt)),w),encrypt(x,generate_key(generate_b_nonce(v))))) ),
inference(res,[status(thm),theory(equality)],[670,19]),
[iquote('0:Res:670.11,19.0')] ).
cnf(968,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ t_holds(key(at,u))
| intruder_message(encrypt(triple(u,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt)) ),
inference(con,[status(thm)],[966]),
[iquote('0:Con:966.2')] ).
cnf(959,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ t_holds(key(at,u))
| intruder_message(pair(encrypt(triple(u,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(v,generate_key(an_a_nonce)))) ),
inference(mrr,[status(thm)],[958,13]),
[iquote('0:MRR:958.3,13.0')] ).
cnf(953,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ a_nonce(v)
| ~ party_of_protocol(x)
| ~ a_stored(pair(x,v))
| ~ t_holds(key(bt,x))
| ~ t_holds(key(at,u))
| intruder_message(pair(encrypt(triple(u,generate_key(v),generate_expiration_time(v)),bt),encrypt(w,generate_key(v)))) ),
inference(res,[status(thm),theory(equality)],[828,19]),
[iquote('0:Res:828.11,19.0')] ).
cnf(828,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ a_nonce(v)
| ~ party_of_protocol(x)
| ~ a_stored(pair(x,v))
| ~ t_holds(key(bt,x))
| ~ t_holds(key(at,u))
| message(sent(a,x,pair(encrypt(triple(u,generate_key(v),generate_expiration_time(v)),bt),encrypt(w,generate_key(v))))) ),
inference(sor,[status(thm)],[123,633]),
[iquote('0:SoR:123.0,633.10')] ).
cnf(913,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ a_nonce(w)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(triple(u,generate_key(w),generate_expiration_time(an_a_nonce)))
| ~ party_of_protocol(x)
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(bt,v))
| ~ a_stored(pair(v,w))
| ~ intruder_holds(key(bt,x))
| b_holds(key(generate_key(w),u)) ),
inference(sor,[status(thm)],[904,33]),
[iquote('0:SoR:904.6,33.3')] ).
cnf(872,plain,
( ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(v)
| ~ party_of_protocol(w)
| message(sent(t,b,triple(encrypt(quadruple(b,generate_b_nonce(v),generate_key(generate_b_nonce(v)),encrypt(triple(w,v,generate_expiration_time(v)),bt)),bt),encrypt(triple(b,generate_key(generate_b_nonce(v)),encrypt(triple(w,v,generate_expiration_time(v)),bt)),bt),u))) ),
inference(con,[status(thm)],[871]),
[iquote('0:Con:871.2')] ).
cnf(887,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(generate_expiration_time(v))
| ~ intruder_message(w)
| ~ intruder_message(u)
| ~ intruder_message(bt)
| ~ intruder_message(x)
| ~ a_nonce(w)
| ~ party_of_protocol(x)
| ~ intruder_message(generate_b_nonce(v))
| ~ intruder_message(generate_key(w))
| ~ b_stored(pair(u,v))
| ~ t_holds(key(bt,x))
| ~ t_holds(key(y,u))
| b_holds(key(generate_key(w),u)) ),
inference(sor,[status(thm)],[582,92]),
[iquote('0:SoR:582.1,92.2')] ).
cnf(869,plain,
( ~ intruder_message(at)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(v)
| ~ party_of_protocol(w)
| message(sent(t,b,triple(encrypt(quadruple(a,generate_b_nonce(v),generate_key(generate_b_nonce(v)),encrypt(triple(w,v,generate_expiration_time(v)),bt)),bt),encrypt(triple(b,generate_key(generate_b_nonce(v)),encrypt(triple(w,v,generate_expiration_time(v)),bt)),at),u))) ),
inference(con,[status(thm)],[868]),
[iquote('0:Con:868.2')] ).
cnf(950,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ a_nonce(w)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(w))
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(bt,v))
| ~ a_stored(pair(v,w))
| b_holds(key(generate_key(w),u)) ),
inference(sor,[status(thm)],[912,29]),
[iquote('0:SoR:912.6,29.3')] ).
cnf(912,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ a_nonce(w)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(triple(u,generate_key(w),generate_expiration_time(an_a_nonce)))
| ~ intruder_message(bt)
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(bt,v))
| ~ a_stored(pair(v,w))
| b_holds(key(generate_key(w),u)) ),
inference(sor,[status(thm)],[904,92]),
[iquote('0:SoR:904.6,92.2')] ).
cnf(936,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ t_holds(key(w,b))
| ~ t_holds(key(at,v))
| intruder_message(encrypt(triple(v,generate_key(an_a_nonce),u),w)) ),
inference(con,[status(thm)],[933]),
[iquote('0:Con:933.3')] ).
cnf(928,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ t_holds(key(w,b))
| ~ t_holds(key(at,v))
| intruder_message(pair(encrypt(triple(v,generate_key(an_a_nonce),u),w),encrypt(x,generate_key(an_a_nonce)))) ),
inference(ssi,[status(thm)],[927,2,111,3,5,79]),
[iquote('0:SSi:927.7,927.6,927.5,927.1,2.0,111.0,3.0,5.0,79.0,2.0,111.0,3.0,5.0,79.0')] ).
cnf(850,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ intruder_message(z)
| ~ a_nonce(v)
| ~ party_of_protocol(z)
| ~ a_stored(pair(z,v))
| ~ t_holds(key(x,z))
| ~ t_holds(key(at,w))
| intruder_message(pair(encrypt(triple(w,generate_key(v),u),x),encrypt(y,generate_key(v)))) ),
inference(res,[status(thm),theory(equality)],[561,19]),
[iquote('0:Res:561.11,19.0')] ).
cnf(904,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ a_nonce(w)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(encrypt(triple(u,generate_key(w),generate_expiration_time(an_a_nonce)),bt))
| ~ b_stored(pair(u,an_a_nonce))
| ~ t_holds(key(bt,v))
| ~ a_stored(pair(v,w))
| b_holds(key(generate_key(w),u)) ),
inference(sor,[status(thm)],[864,112]),
[iquote('0:SoR:864.6,112.0')] ).
cnf(864,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ a_nonce(w)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(generate_b_nonce(x))
| ~ intruder_message(encrypt(triple(u,generate_key(w),generate_expiration_time(x)),bt))
| ~ b_stored(pair(u,x))
| ~ t_holds(key(bt,v))
| ~ a_stored(pair(v,w))
| b_holds(key(generate_key(w),u)) ),
inference(ssi,[status(thm)],[862,8]),
[iquote('0:SSi:862.1,8.0')] ).
cnf(209,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(triple(x,v,y))
| ~ t_holds(key(z,x))
| ~ t_holds(key(generate_key(an_a_nonce),u))
| message(sent(t,x,triple(encrypt(quadruple(u,v,generate_key(v),y),z),encrypt(triple(x,generate_key(v),y),generate_key(an_a_nonce)),w))) ),
inference(sor,[status(thm)],[150,207]),
[iquote('0:SoR:150.4,207.1')] ).
cnf(582,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(encrypt(generate_b_nonce(v),generate_key(w)))
| ~ intruder_message(generate_expiration_time(v))
| ~ intruder_message(w)
| ~ intruder_message(u)
| ~ intruder_message(bt)
| ~ intruder_message(x)
| ~ a_nonce(w)
| ~ party_of_protocol(x)
| ~ b_stored(pair(u,v))
| ~ t_holds(key(bt,x))
| ~ t_holds(key(y,u))
| b_holds(key(generate_key(w),u)) ),
inference(ssi,[status(thm)],[572,8]),
[iquote('0:SSi:572.1,8.0')] ).
cnf(876,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ a_nonce(w)
| ~ intruder_message(generate_b_nonce(x))
| ~ intruder_message(u)
| ~ intruder_message(generate_key(w))
| ~ intruder_message(generate_expiration_time(x))
| ~ b_stored(pair(u,x))
| ~ intruder_holds(key(bt,v))
| ~ a_stored(pair(b,w))
| b_holds(key(generate_key(w),u)) ),
inference(sor,[status(thm)],[442,29]),
[iquote('0:SoR:442.1,29.3')] ).
cnf(880,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ party_of_protocol(x)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(v))
| ~ intruder_message(generate_expiration_time(w))
| ~ a_stored(pair(b,v))
| ~ intruder_holds(key(bt,x))
| b_holds(key(generate_key(v),u)) ),
inference(mrr,[status(thm)],[879,100]),
[iquote('0:MRR:879.10,100.4')] ).
cnf(800,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(triple(u,generate_key(v),generate_expiration_time(w)))
| ~ party_of_protocol(x)
| ~ b_stored(pair(u,w))
| ~ a_stored(pair(b,v))
| ~ intruder_holds(key(bt,x))
| b_holds(key(generate_key(v),u)) ),
inference(sor,[status(thm)],[730,33]),
[iquote('0:SoR:730.4,33.3')] ).
cnf(811,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ party_of_protocol(w)
| ~ a_stored(pair(w,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(u,w))
| ~ t_holds(key(at,b))
| intruder_message(pair(encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),u),encrypt(v,generate_key(generate_b_nonce(an_a_nonce))))) ),
inference(res,[status(thm),theory(equality)],[610,19]),
[iquote('0:Res:610.7,19.0')] ).
cnf(787,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ party_of_protocol(y)
| ~ a_stored(pair(y,generate_b_nonce(w)))
| ~ t_holds(key(x,y))
| ~ t_holds(key(at,b))
| message(sent(a,y,pair(u,encrypt(v,generate_key(generate_b_nonce(w)))))) ),
inference(con,[status(thm)],[783]),
[iquote('0:Con:783.2')] ).
cnf(442,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(triple(u,generate_key(v),generate_expiration_time(w)))
| ~ party_of_protocol(x)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ intruder_message(generate_b_nonce(w))
| ~ b_stored(pair(u,w))
| ~ intruder_holds(key(bt,x))
| ~ a_stored(pair(b,v))
| b_holds(key(generate_key(v),u)) ),
inference(ssi,[status(thm)],[434,8]),
[iquote('0:SSi:434.1,8.0')] ).
cnf(719,plain,
( ~ intruder_message(generate_expiration_time(u))
| ~ intruder_message(v)
| ~ intruder_message(bt)
| ~ intruder_message(w)
| ~ a_nonce(v)
| ~ party_of_protocol(w)
| ~ intruder_message(generate_b_nonce(u))
| ~ party_of_protocol(x)
| ~ b_stored(pair(b,u))
| ~ t_holds(key(bt,w))
| ~ intruder_holds(key(generate_key(v),x))
| b_holds(key(generate_key(v),b)) ),
inference(sor,[status(thm)],[630,33]),
[iquote('0:SoR:630.0,33.3')] ).
cnf(711,plain,
( ~ intruder_message(generate_expiration_time(u))
| ~ intruder_message(v)
| ~ intruder_message(bt)
| ~ intruder_message(w)
| ~ a_nonce(v)
| ~ party_of_protocol(w)
| ~ intruder_message(generate_b_nonce(u))
| ~ party_of_protocol(x)
| ~ b_stored(pair(a,u))
| ~ t_holds(key(bt,w))
| ~ intruder_holds(key(generate_key(v),x))
| b_holds(key(generate_key(v),a)) ),
inference(sor,[status(thm)],[597,33]),
[iquote('0:SoR:597.0,33.3')] ).
cnf(670,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ party_of_protocol(y)
| ~ a_stored(pair(y,generate_b_nonce(v)))
| ~ t_holds(key(w,y))
| ~ t_holds(key(at,b))
| message(sent(a,y,pair(encrypt(triple(b,generate_key(generate_b_nonce(v)),encrypt(triple(u,v,generate_expiration_time(v)),bt)),w),encrypt(x,generate_key(generate_b_nonce(v)))))) ),
inference(sor,[status(thm)],[123,458]),
[iquote('0:SoR:123.0,458.10')] ).
cnf(874,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ party_of_protocol(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(generate_key(u))
| ~ intruder_message(generate_expiration_time(w))
| ~ a_stored(pair(b,u))
| ~ b_stored(pair(a,w))
| ~ intruder_holds(key(bt,v))
| b_holds(key(generate_key(u),a)) ),
inference(ssi,[status(thm)],[873,1,78]),
[iquote('0:SSi:873.6,1.0,78.0')] ).
cnf(816,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ intruder_message(triple(a,generate_key(u),generate_expiration_time(v)))
| ~ party_of_protocol(w)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_stored(pair(b,u))
| ~ b_stored(pair(a,v))
| ~ intruder_holds(key(bt,w))
| b_holds(key(generate_key(u),a)) ),
inference(sor,[status(thm)],[481,145]),
[iquote('0:SoR:481.0,145.2')] ).
cnf(788,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ party_of_protocol(w)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(v))
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ b_stored(pair(u,an_a_nonce))
| ~ a_stored(pair(b,v))
| ~ intruder_holds(key(bt,w))
| b_holds(key(generate_key(v),u)) ),
inference(sor,[status(thm)],[740,29]),
[iquote('0:SoR:740.4,29.3')] ).
cnf(699,plain,
( ~ intruder_message(u)
| ~ party_of_protocol(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ fresh_to_b(w)
| ~ party_of_protocol(x)
| ~ intruder_holds(key(bt,v))
| message(sent(t,b,triple(encrypt(quadruple(b,generate_b_nonce(w),generate_key(generate_b_nonce(w)),encrypt(triple(x,w,generate_expiration_time(w)),bt)),bt),encrypt(triple(b,generate_key(generate_b_nonce(w)),encrypt(triple(x,w,generate_expiration_time(w)),bt)),bt),u))) ),
inference(ssi,[status(thm)],[696,2,111]),
[iquote('0:SSi:696.1,696.0,2.0,111.0,2.0,111.0')] ).
cnf(763,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(bt)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ intruder_message(generate_b_nonce(w))
| ~ intruder_message(u)
| ~ intruder_message(generate_key(v))
| ~ intruder_message(generate_expiration_time(w))
| ~ b_stored(pair(u,w))
| ~ a_stored(pair(b,v))
| b_holds(key(generate_key(v),u)) ),
inference(sor,[status(thm)],[441,29]),
[iquote('0:SoR:441.1,29.3')] ).
cnf(771,plain,
( ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ party_of_protocol(v)
| message(sent(t,b,triple(encrypt(quadruple(b,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),bt),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),bt),u))) ),
inference(obv,[status(thm),theory(equality)],[770]),
[iquote('0:Obv:770.0')] ).
cnf(762,plain,
( ~ intruder_message(at)
| ~ intruder_message(u)
| ~ party_of_protocol(v)
| message(sent(t,b,triple(encrypt(quadruple(a,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),bt),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),at),u))) ),
inference(obv,[status(thm),theory(equality)],[761]),
[iquote('0:Obv:761.0')] ).
cnf(866,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(v))
| ~ intruder_message(generate_expiration_time(w))
| ~ a_stored(pair(b,v))
| b_holds(key(generate_key(v),u)) ),
inference(mrr,[status(thm)],[865,100]),
[iquote('0:MRR:865.10,100.4')] ).
cnf(698,plain,
( ~ intruder_message(u)
| ~ party_of_protocol(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ fresh_to_b(w)
| ~ party_of_protocol(x)
| ~ intruder_holds(key(at,v))
| message(sent(t,b,triple(encrypt(quadruple(a,generate_b_nonce(w),generate_key(generate_b_nonce(w)),encrypt(triple(x,w,generate_expiration_time(w)),bt)),bt),encrypt(triple(b,generate_key(generate_b_nonce(w)),encrypt(triple(x,w,generate_expiration_time(w)),bt)),at),u))) ),
inference(ssi,[status(thm)],[697,1,78]),
[iquote('0:SSi:697.1,697.0,1.0,78.0,1.0,78.0')] ).
cnf(799,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(triple(u,generate_key(v),generate_expiration_time(w)))
| ~ intruder_message(bt)
| ~ b_stored(pair(u,w))
| ~ a_stored(pair(b,v))
| b_holds(key(generate_key(v),u)) ),
inference(sor,[status(thm)],[730,92]),
[iquote('0:SoR:730.4,92.2')] ).
cnf(855,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ a_nonce(w)
| ~ party_of_protocol(x)
| ~ a_stored(pair(x,w))
| ~ t_holds(key(bt,x))
| intruder_message(pair(u,encrypt(v,generate_key(w)))) ),
inference(res,[status(thm),theory(equality)],[846,19]),
[iquote('0:Res:846.9,19.0')] ).
cnf(846,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ a_nonce(w)
| ~ party_of_protocol(x)
| ~ a_stored(pair(x,w))
| ~ t_holds(key(bt,x))
| message(sent(a,x,pair(u,encrypt(v,generate_key(w))))) ),
inference(sor,[status(thm)],[137,844]),
[iquote('0:SoR:137.0,844.6')] ).
cnf(845,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ t_holds(key(bt,u))
| intruder_message(encrypt(quadruple(u,v,generate_key(v),generate_expiration_time(v)),bt)) ),
inference(ssi,[status(thm)],[842,2,111]),
[iquote('0:SSi:842.6,842.4,2.0,111.0,2.0,111.0')] ).
cnf(561,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ intruder_message(z)
| ~ a_nonce(v)
| ~ party_of_protocol(z)
| ~ a_stored(pair(z,v))
| ~ t_holds(key(x,z))
| ~ t_holds(key(at,w))
| message(sent(a,z,pair(encrypt(triple(w,generate_key(v),u),x),encrypt(y,generate_key(v))))) ),
inference(sor,[status(thm)],[123,387]),
[iquote('0:SoR:123.0,387.10')] ).
cnf(844,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ t_holds(key(bt,u))
| intruder_message(encrypt(quadruple(u,v,generate_key(v),generate_expiration_time(v)),at)) ),
inference(ssi,[status(thm)],[843,1,78]),
[iquote('0:SSi:843.6,843.4,1.0,78.0,1.0,78.0')] ).
cnf(834,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ fresh_to_b(v)
| ~ party_of_protocol(w)
| ~ t_holds(key(x,w))
| ~ t_holds(key(bt,u))
| intruder_message(encrypt(quadruple(u,v,generate_key(v),generate_expiration_time(v)),x)) ),
inference(con,[status(thm)],[830]),
[iquote('0:Con:830.3')] ).
cnf(839,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ party_of_protocol(v)
| ~ intruder_message(generate_key(u))
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ a_stored(pair(b,u))
| ~ intruder_holds(key(bt,v))
| b_holds(key(generate_key(u),a)) ),
inference(ssi,[status(thm)],[838,1,78]),
[iquote('0:SSi:838.4,1.0,78.0')] ).
cnf(818,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ intruder_message(triple(a,generate_key(u),generate_expiration_time(an_a_nonce)))
| ~ party_of_protocol(v)
| ~ a_stored(pair(b,u))
| ~ intruder_holds(key(bt,v))
| b_holds(key(generate_key(u),a)) ),
inference(mrr,[status(thm)],[817,88]),
[iquote('0:MRR:817.6,88.0')] ).
cnf(633,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(v)
| ~ intruder_message(x)
| ~ fresh_to_b(v)
| ~ party_of_protocol(x)
| ~ t_holds(key(y,x))
| ~ t_holds(key(bt,u))
| intruder_message(triple(encrypt(quadruple(u,v,generate_key(v),generate_expiration_time(v)),y),encrypt(triple(x,generate_key(v),generate_expiration_time(v)),bt),w)) ),
inference(res,[status(thm),theory(equality)],[196,19]),
[iquote('0:Res:196.10,19.0')] ).
cnf(481,plain,
( ~ intruder_message(generate_b_nonce(u))
| ~ a_nonce(v)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ intruder_message(triple(a,generate_key(v),generate_expiration_time(u)))
| ~ party_of_protocol(w)
| ~ a_stored(pair(b,v))
| ~ b_stored(pair(a,u))
| ~ intruder_holds(key(bt,w))
| b_holds(key(generate_key(v),a)) ),
inference(sor,[status(thm)],[422,33]),
[iquote('0:SoR:422.0,33.3')] ).
cnf(815,plain,
( ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(u)
| ~ party_of_protocol(v)
| intruder_message(encrypt(quadruple(b,generate_b_nonce(u),generate_key(generate_b_nonce(u)),encrypt(triple(v,u,generate_expiration_time(u)),bt)),bt)) ),
inference(ssi,[status(thm)],[812,2,111]),
[iquote('0:SSi:812.1,812.0,2.0,111.0,2.0,111.0')] ).
cnf(814,plain,
( ~ intruder_message(at)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(u)
| ~ party_of_protocol(v)
| intruder_message(encrypt(quadruple(a,generate_b_nonce(u),generate_key(generate_b_nonce(u)),encrypt(triple(v,u,generate_expiration_time(u)),bt)),bt)) ),
inference(ssi,[status(thm)],[813,1,78]),
[iquote('0:SSi:813.1,813.0,1.0,78.0,1.0,78.0')] ).
cnf(785,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ fresh_to_b(w)
| ~ party_of_protocol(x)
| ~ t_holds(key(v,u))
| intruder_message(encrypt(quadruple(u,generate_b_nonce(w),generate_key(generate_b_nonce(w)),encrypt(triple(x,w,generate_expiration_time(w)),bt)),bt)) ),
inference(res,[status(thm),theory(equality)],[13,677]),
[iquote('0:Res:13.0,677.7')] ).
cnf(610,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ party_of_protocol(w)
| ~ a_stored(pair(w,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(u,w))
| ~ t_holds(key(at,b))
| message(sent(a,w,pair(encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),u),encrypt(v,generate_key(generate_b_nonce(an_a_nonce)))))) ),
inference(sor,[status(thm)],[123,400]),
[iquote('0:SoR:123.0,400.6')] ).
cnf(730,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ intruder_message(encrypt(triple(u,generate_key(v),generate_expiration_time(w)),bt))
| ~ fresh_to_b(w)
| ~ intruder_message(w)
| ~ b_stored(pair(u,w))
| ~ a_stored(pair(b,v))
| b_holds(key(generate_key(v),u)) ),
inference(sor,[status(thm)],[430,145]),
[iquote('0:SoR:430.4,145.2')] ).
cnf(790,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ a_nonce(w)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(w))
| ~ intruder_message(generate_expiration_time(w))
| ~ intruder_holds(key(bt,v))
| ~ a_stored(pair(b,w))
| b_holds(key(generate_key(w),u)) ),
inference(mrr,[status(thm)],[789,100]),
[iquote('0:MRR:789.8,100.4')] ).
cnf(276,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(triple(u,generate_key(v),generate_expiration_time(v)))
| ~ party_of_protocol(w)
| ~ a_nonce(v)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ b_stored(pair(u,v))
| ~ intruder_holds(key(bt,w))
| ~ a_stored(pair(b,v))
| b_holds(key(generate_key(v),u)) ),
inference(ssi,[status(thm)],[270,8]),
[iquote('0:SSi:270.1,8.0')] ).
cnf(740,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ intruder_message(triple(u,generate_key(v),generate_expiration_time(an_a_nonce)))
| ~ party_of_protocol(w)
| ~ b_stored(pair(u,an_a_nonce))
| ~ a_stored(pair(b,v))
| ~ intruder_holds(key(bt,w))
| b_holds(key(generate_key(v),u)) ),
inference(sor,[status(thm)],[731,33]),
[iquote('0:SoR:731.4,33.3')] ).
cnf(677,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ fresh_to_b(w)
| ~ party_of_protocol(x)
| ~ t_holds(key(y,b))
| ~ t_holds(key(v,u))
| intruder_message(encrypt(quadruple(u,generate_b_nonce(w),generate_key(generate_b_nonce(w)),encrypt(triple(x,w,generate_expiration_time(w)),bt)),y)) ),
inference(con,[status(thm)],[672]),
[iquote('0:Con:672.2')] ).
cnf(729,plain,
( ~ intruder_message(generate_expiration_time(u))
| ~ intruder_message(v)
| ~ intruder_message(bt)
| ~ intruder_message(generate_b_nonce(u))
| ~ intruder_message(w)
| ~ a_nonce(v)
| ~ party_of_protocol(w)
| ~ b_stored(pair(a,u))
| ~ a_stored(pair(w,v))
| ~ t_holds(key(bt,w))
| b_holds(key(generate_key(v),a)) ),
inference(ssi,[status(thm)],[724,8,1,78]),
[iquote('0:SSi:724.1,724.0,8.0,1.0,78.0')] ).
cnf(781,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ a_nonce(u)
| ~ party_of_protocol(v)
| ~ a_stored(pair(v,u))
| ~ t_holds(key(bt,v))
| b_holds(key(generate_key(u),a)) ),
inference(ssi,[status(thm)],[780,1,78]),
[iquote('0:SSi:780.1,780.0,1.0,78.0,1.0,78.0')] ).
cnf(768,plain,
( ~ a_nonce(u)
| ~ intruder_message(v)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ a_stored(pair(b,u))
| intruder_message(pair(encrypt(triple(a,generate_key(u),generate_expiration_time(u)),bt),encrypt(v,generate_key(u)))) ),
inference(ssi,[status(thm)],[767,2,111]),
[iquote('0:SSi:767.2,767.0,2.0,111.0,2.0,111.0')] ).
cnf(653,plain,
( ~ intruder_message(u)
| ~ party_of_protocol(v)
| ~ intruder_holds(key(bt,v))
| message(sent(t,b,triple(encrypt(quadruple(b,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),bt),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),bt),u))) ),
inference(ssi,[status(thm)],[650,2,111]),
[iquote('0:SSi:650.1,650.0,2.0,111.0,2.0,111.0')] ).
cnf(749,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ t_holds(key(bt,u))
| ~ a_stored(pair(u,v))
| intruder_message(pair(encrypt(triple(a,generate_key(v),generate_expiration_time(v)),bt),encrypt(w,generate_key(v)))) ),
inference(res,[status(thm),theory(equality)],[640,19]),
[iquote('0:Res:640.8,19.0')] ).
cnf(441,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(triple(u,generate_key(v),generate_expiration_time(w)))
| ~ intruder_message(bt)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ intruder_message(generate_b_nonce(w))
| ~ b_stored(pair(u,w))
| ~ a_stored(pair(b,v))
| b_holds(key(generate_key(v),u)) ),
inference(ssi,[status(thm)],[435,8]),
[iquote('0:SSi:435.1,8.0')] ).
cnf(654,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ party_of_protocol(x)
| ~ a_stored(pair(x,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(w,x))
| ~ t_holds(key(at,b))
| message(sent(a,x,pair(u,encrypt(v,generate_key(generate_b_nonce(an_a_nonce)))))) ),
inference(sor,[status(thm)],[137,617]),
[iquote('0:SoR:137.0,617.5')] ).
cnf(718,plain,
( ~ intruder_message(generate_expiration_time(u))
| ~ intruder_message(v)
| ~ intruder_message(bt)
| ~ intruder_message(w)
| ~ a_nonce(v)
| ~ party_of_protocol(w)
| ~ intruder_message(generate_b_nonce(u))
| ~ intruder_message(generate_key(v))
| ~ b_stored(pair(b,u))
| ~ t_holds(key(bt,w))
| b_holds(key(generate_key(v),b)) ),
inference(sor,[status(thm)],[630,92]),
[iquote('0:SoR:630.0,92.2')] ).
cnf(652,plain,
( ~ intruder_message(u)
| ~ party_of_protocol(v)
| ~ intruder_holds(key(at,v))
| message(sent(t,b,triple(encrypt(quadruple(a,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),bt),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),at),u))) ),
inference(ssi,[status(thm)],[651,1,78]),
[iquote('0:SSi:651.1,651.0,1.0,78.0,1.0,78.0')] ).
cnf(710,plain,
( ~ intruder_message(generate_expiration_time(u))
| ~ intruder_message(v)
| ~ intruder_message(bt)
| ~ intruder_message(w)
| ~ a_nonce(v)
| ~ party_of_protocol(w)
| ~ intruder_message(generate_b_nonce(u))
| ~ intruder_message(generate_key(v))
| ~ b_stored(pair(a,u))
| ~ t_holds(key(bt,w))
| b_holds(key(generate_key(v),a)) ),
inference(sor,[status(thm)],[597,92]),
[iquote('0:SoR:597.0,92.2')] ).
cnf(759,plain,
( ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(u)
| ~ party_of_protocol(v)
| intruder_message(encrypt(triple(b,generate_key(generate_b_nonce(u)),encrypt(triple(v,u,generate_expiration_time(u)),bt)),bt)) ),
inference(ssi,[status(thm)],[756,2,111]),
[iquote('0:SSi:756.1,756.0,2.0,111.0,2.0,111.0')] ).
cnf(758,plain,
( ~ intruder_message(at)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(u)
| ~ party_of_protocol(v)
| intruder_message(encrypt(triple(b,generate_key(generate_b_nonce(u)),encrypt(triple(v,u,generate_expiration_time(u)),bt)),at)) ),
inference(ssi,[status(thm)],[757,1,78]),
[iquote('0:SSi:757.1,757.0,1.0,78.0,1.0,78.0')] ).
cnf(753,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ fresh_to_b(w)
| ~ party_of_protocol(x)
| ~ t_holds(key(v,u))
| intruder_message(encrypt(triple(b,generate_key(generate_b_nonce(w)),encrypt(triple(x,w,generate_expiration_time(w)),bt)),v)) ),
inference(res,[status(thm),theory(equality)],[13,676]),
[iquote('0:Res:13.0,676.7')] ).
cnf(695,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ a_nonce(w)
| ~ party_of_protocol(y)
| ~ a_stored(pair(y,w))
| ~ t_holds(key(x,y))
| message(sent(a,y,pair(u,encrypt(v,generate_key(w))))) ),
inference(con,[status(thm)],[688]),
[iquote('0:Con:688.2')] ).
cnf(750,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(v))
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ b_stored(pair(u,an_a_nonce))
| ~ a_stored(pair(b,v))
| b_holds(key(generate_key(v),u)) ),
inference(sor,[status(thm)],[739,29]),
[iquote('0:SoR:739.4,29.3')] ).
cnf(739,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ intruder_message(triple(u,generate_key(v),generate_expiration_time(an_a_nonce)))
| ~ intruder_message(bt)
| ~ b_stored(pair(u,an_a_nonce))
| ~ a_stored(pair(b,v))
| b_holds(key(generate_key(v),u)) ),
inference(sor,[status(thm)],[731,92]),
[iquote('0:SoR:731.4,92.2')] ).
cnf(640,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ t_holds(key(bt,u))
| ~ a_stored(pair(u,v))
| message(sent(a,u,pair(encrypt(triple(a,generate_key(v),generate_expiration_time(v)),bt),encrypt(w,generate_key(v))))) ),
inference(mrr,[status(thm)],[639,12]),
[iquote('0:MRR:639.6,12.0')] ).
cnf(731,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ intruder_message(encrypt(triple(u,generate_key(v),generate_expiration_time(an_a_nonce)),bt))
| ~ b_stored(pair(u,an_a_nonce))
| ~ a_stored(pair(b,v))
| b_holds(key(generate_key(v),u)) ),
inference(sor,[status(thm)],[430,112]),
[iquote('0:SoR:430.4,112.0')] ).
cnf(430,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ intruder_message(generate_b_nonce(w))
| ~ intruder_message(encrypt(triple(u,generate_key(v),generate_expiration_time(w)),bt))
| ~ b_stored(pair(u,w))
| ~ a_stored(pair(b,v))
| b_holds(key(generate_key(v),u)) ),
inference(ssi,[status(thm)],[426,8]),
[iquote('0:SSi:426.1,8.0')] ).
cnf(728,plain,
( ~ a_nonce(u)
| ~ intruder_message(v)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ a_stored(pair(b,u))
| intruder_message(pair(encrypt(triple(a,generate_key(u),w),bt),encrypt(v,generate_key(u)))) ),
inference(ssi,[status(thm)],[725,2,111]),
[iquote('0:SSi:725.2,725.0,2.0,111.0,2.0,111.0')] ).
cnf(727,plain,
( ~ a_nonce(u)
| ~ intruder_message(v)
| ~ intruder_message(at)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ a_stored(pair(a,u))
| intruder_message(pair(encrypt(triple(a,generate_key(u),w),at),encrypt(v,generate_key(u)))) ),
inference(ssi,[status(thm)],[726,1,78]),
[iquote('0:SSi:726.2,726.0,1.0,78.0,1.0,78.0')] ).
cnf(525,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(v)
| ~ intruder_message(y)
| ~ t_holds(key(x,u))
| ~ a_stored(pair(u,v))
| intruder_message(pair(encrypt(triple(a,generate_key(v),y),x),encrypt(w,generate_key(v)))) ),
inference(res,[status(thm),theory(equality)],[394,19]),
[iquote('0:Res:394.9,19.0')] ).
cnf(630,plain,
( ~ intruder_message(encrypt(generate_b_nonce(u),generate_key(v)))
| ~ intruder_message(generate_expiration_time(u))
| ~ intruder_message(v)
| ~ intruder_message(bt)
| ~ intruder_message(w)
| ~ a_nonce(v)
| ~ party_of_protocol(w)
| ~ b_stored(pair(b,u))
| ~ t_holds(key(bt,w))
| b_holds(key(generate_key(v),b)) ),
inference(ssi,[status(thm)],[620,8,2,111]),
[iquote('0:SSi:620.1,620.0,8.0,2.0,111.0')] ).
cnf(597,plain,
( ~ intruder_message(encrypt(generate_b_nonce(u),generate_key(v)))
| ~ intruder_message(generate_expiration_time(u))
| ~ intruder_message(v)
| ~ intruder_message(bt)
| ~ intruder_message(w)
| ~ a_nonce(v)
| ~ party_of_protocol(w)
| ~ b_stored(pair(a,u))
| ~ t_holds(key(bt,w))
| b_holds(key(generate_key(v),a)) ),
inference(ssi,[status(thm)],[587,8,1,78]),
[iquote('0:SSi:587.1,587.0,8.0,1.0,78.0')] ).
cnf(705,plain,
( ~ intruder_message(bt)
| ~ a_nonce(u)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ intruder_message(u)
| ~ intruder_message(x)
| message(sent(t,b,triple(encrypt(quadruple(b,u,generate_key(u),x),bt),encrypt(triple(b,generate_key(u),x),bt),v))) ),
inference(obv,[status(thm),theory(equality)],[704]),
[iquote('0:Obv:704.0')] ).
cnf(703,plain,
( ~ a_nonce(u)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(v)
| intruder_message(encrypt(quadruple(b,u,generate_key(u),v),bt)) ),
inference(ssi,[status(thm)],[700,2,111]),
[iquote('0:SSi:700.2,700.0,2.0,111.0,2.0,111.0')] ).
cnf(547,plain,
( ~ a_nonce(u)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ intruder_message(u)
| ~ intruder_message(x)
| ~ intruder_holds(key(bt,w))
| message(sent(t,b,triple(encrypt(quadruple(b,u,generate_key(u),x),bt),encrypt(triple(b,generate_key(u),x),bt),v))) ),
inference(ssi,[status(thm)],[544,2,111]),
[iquote('0:SSi:544.2,544.0,2.0,111.0,2.0,111.0')] ).
cnf(702,plain,
( ~ a_nonce(u)
| ~ intruder_message(at)
| ~ intruder_message(u)
| ~ intruder_message(v)
| intruder_message(encrypt(quadruple(a,u,generate_key(u),v),bt)) ),
inference(ssi,[status(thm)],[701,1,78]),
[iquote('0:SSi:701.2,701.0,1.0,78.0,1.0,78.0')] ).
cnf(685,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(v)
| ~ intruder_message(x)
| ~ t_holds(key(w,u))
| intruder_message(encrypt(quadruple(u,v,generate_key(v),x),bt)) ),
inference(ssi,[status(thm)],[682,2,111]),
[iquote('0:SSi:682.4,2.0,111.0')] ).
cnf(693,plain,
( ~ a_nonce(u)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(v)
| intruder_message(encrypt(quadruple(b,u,generate_key(u),v),at)) ),
inference(ssi,[status(thm)],[690,2,111]),
[iquote('0:SSi:690.2,690.0,2.0,111.0,2.0,111.0')] ).
cnf(692,plain,
( ~ a_nonce(u)
| ~ intruder_message(at)
| ~ intruder_message(u)
| ~ intruder_message(v)
| intruder_message(encrypt(quadruple(a,u,generate_key(u),v),at)) ),
inference(ssi,[status(thm)],[691,1,78]),
[iquote('0:SSi:691.2,691.0,1.0,78.0,1.0,78.0')] ).
cnf(470,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ fresh_to_b(x)
| ~ party_of_protocol(y)
| ~ t_holds(key(z,u))
| ~ intruder_holds(key(z,w))
| message(sent(t,b,triple(encrypt(quadruple(u,generate_b_nonce(x),generate_key(generate_b_nonce(x)),encrypt(triple(y,x,generate_expiration_time(x)),bt)),bt),encrypt(triple(b,generate_key(generate_b_nonce(x)),encrypt(triple(y,x,generate_expiration_time(x)),bt)),z),v))) ),
inference(res,[status(thm),theory(equality)],[13,295]),
[iquote('0:Res:13.0,295.8')] ).
cnf(684,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(v)
| ~ intruder_message(x)
| ~ t_holds(key(w,u))
| intruder_message(encrypt(quadruple(u,v,generate_key(v),x),at)) ),
inference(ssi,[status(thm)],[683,1,78]),
[iquote('0:SSi:683.4,1.0,78.0')] ).
cnf(567,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(v)
| ~ intruder_message(y)
| ~ t_holds(key(z,x))
| ~ t_holds(key(w,u))
| intruder_message(encrypt(quadruple(u,v,generate_key(v),y),z)) ),
inference(con,[status(thm)],[563]),
[iquote('0:Con:563.3')] ).
cnf(675,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ party_of_protocol(w)
| ~ a_stored(pair(w,generate_b_nonce(u)))
| ~ t_holds(key(v,w))
| ~ t_holds(key(at,b))
| a_holds(key(generate_key(generate_b_nonce(u)),w)) ),
inference(con,[status(thm)],[671]),
[iquote('0:Con:671.0')] ).
cnf(660,plain,
( ~ intruder_message(bt)
| intruder_message(encrypt(quadruple(b,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),bt)) ),
inference(ssi,[status(thm)],[657,2,111]),
[iquote('0:SSi:657.1,657.0,2.0,111.0,2.0,111.0')] ).
cnf(458,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ fresh_to_b(x)
| ~ party_of_protocol(y)
| ~ t_holds(key(z,b))
| ~ t_holds(key(w,u))
| intruder_message(triple(encrypt(quadruple(u,generate_b_nonce(x),generate_key(generate_b_nonce(x)),encrypt(triple(y,x,generate_expiration_time(x)),bt)),z),encrypt(triple(b,generate_key(generate_b_nonce(x)),encrypt(triple(y,x,generate_expiration_time(x)),bt)),w),v)) ),
inference(res,[status(thm),theory(equality)],[269,19]),
[iquote('0:Res:269.10,19.0')] ).
cnf(659,plain,
( ~ intruder_message(at)
| intruder_message(encrypt(quadruple(a,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),bt)) ),
inference(ssi,[status(thm)],[658,1,78]),
[iquote('0:SSi:658.1,658.0,1.0,78.0,1.0,78.0')] ).
cnf(656,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ t_holds(key(v,u))
| intruder_message(encrypt(quadruple(u,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),bt)) ),
inference(res,[status(thm),theory(equality)],[13,617]),
[iquote('0:Res:13.0,617.3')] ).
cnf(617,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ t_holds(key(w,b))
| ~ t_holds(key(v,u))
| intruder_message(encrypt(quadruple(u,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),w)) ),
inference(con,[status(thm)],[612]),
[iquote('0:Con:612.2')] ).
cnf(648,plain,
( ~ intruder_message(bt)
| intruder_message(encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),bt)) ),
inference(ssi,[status(thm)],[645,2,111]),
[iquote('0:SSi:645.1,645.0,2.0,111.0,2.0,111.0')] ).
cnf(443,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ t_holds(key(x,u))
| ~ intruder_holds(key(x,w))
| message(sent(t,b,triple(encrypt(quadruple(u,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),bt),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),x),v))) ),
inference(res,[status(thm),theory(equality)],[13,294]),
[iquote('0:Res:13.0,294.4')] ).
cnf(647,plain,
( ~ intruder_message(at)
| intruder_message(encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),at)) ),
inference(ssi,[status(thm)],[646,1,78]),
[iquote('0:SSi:646.1,646.0,1.0,78.0,1.0,78.0')] ).
cnf(642,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ t_holds(key(v,u))
| intruder_message(encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),v)) ),
inference(res,[status(thm),theory(equality)],[13,616]),
[iquote('0:Res:13.0,616.3')] ).
cnf(638,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ t_holds(key(bt,u))
| ~ a_stored(pair(u,v))
| a_holds(key(generate_key(v),u)) ),
inference(mrr,[status(thm)],[637,12]),
[iquote('0:MRR:637.5,12.0')] ).
cnf(196,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(v)
| ~ intruder_message(x)
| ~ fresh_to_b(v)
| ~ party_of_protocol(x)
| ~ t_holds(key(y,x))
| ~ t_holds(key(bt,u))
| message(sent(t,x,triple(encrypt(quadruple(u,v,generate_key(v),generate_expiration_time(v)),y),encrypt(triple(x,generate_key(v),generate_expiration_time(v)),bt),w))) ),
inference(sor,[status(thm)],[150,144]),
[iquote('0:SoR:150.4,144.4')] ).
cnf(629,plain,
( ~ a_nonce(u)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(v)
| intruder_message(encrypt(triple(b,generate_key(u),v),bt)) ),
inference(ssi,[status(thm)],[626,2,111]),
[iquote('0:SSi:626.2,626.0,2.0,111.0,2.0,111.0')] ).
cnf(628,plain,
( ~ a_nonce(u)
| ~ intruder_message(at)
| ~ intruder_message(u)
| ~ intruder_message(v)
| intruder_message(encrypt(triple(b,generate_key(u),v),at)) ),
inference(ssi,[status(thm)],[627,1,78]),
[iquote('0:SSi:627.2,627.0,1.0,78.0,1.0,78.0')] ).
cnf(581,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(v)
| ~ intruder_message(x)
| ~ t_holds(key(w,u))
| intruder_message(encrypt(triple(b,generate_key(v),x),w)) ),
inference(ssi,[status(thm)],[578,2,111]),
[iquote('0:SSi:578.4,2.0,111.0')] ).
cnf(615,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ party_of_protocol(v)
| ~ a_stored(pair(v,generate_b_nonce(an_a_nonce)))
| ~ t_holds(key(u,v))
| ~ t_holds(key(at,b))
| a_holds(key(generate_key(generate_b_nonce(an_a_nonce)),v)) ),
inference(con,[status(thm)],[611]),
[iquote('0:Con:611.1')] ).
cnf(400,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ t_holds(key(x,b))
| ~ t_holds(key(w,u))
| intruder_message(triple(encrypt(quadruple(u,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),x),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),w),v)) ),
inference(res,[status(thm),theory(equality)],[268,19]),
[iquote('0:Res:268.6,19.0')] ).
cnf(596,plain,
( ~ a_nonce(u)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(v)
| intruder_message(encrypt(triple(a,generate_key(u),v),bt)) ),
inference(ssi,[status(thm)],[593,2,111]),
[iquote('0:SSi:593.2,593.0,2.0,111.0,2.0,111.0')] ).
cnf(595,plain,
( ~ a_nonce(u)
| ~ intruder_message(at)
| ~ intruder_message(u)
| ~ intruder_message(v)
| intruder_message(encrypt(triple(a,generate_key(u),v),at)) ),
inference(ssi,[status(thm)],[594,1,78]),
[iquote('0:SSi:594.2,594.0,1.0,78.0,1.0,78.0')] ).
cnf(580,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(v)
| ~ intruder_message(x)
| ~ t_holds(key(w,u))
| intruder_message(encrypt(triple(a,generate_key(v),x),w)) ),
inference(ssi,[status(thm)],[579,1,78]),
[iquote('0:SSi:579.4,1.0,78.0')] ).
cnf(566,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(v)
| ~ intruder_message(y)
| ~ t_holds(key(z,x))
| ~ t_holds(key(w,u))
| intruder_message(encrypt(triple(x,generate_key(v),y),w)) ),
inference(con,[status(thm)],[564]),
[iquote('0:Con:564.3')] ).
cnf(387,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ intruder_message(v)
| ~ intruder_message(z)
| ~ t_holds(key(x1,y))
| ~ t_holds(key(x,u))
| intruder_message(triple(encrypt(quadruple(u,v,generate_key(v),z),x1),encrypt(triple(y,generate_key(v),z),x),w)) ),
inference(res,[status(thm),theory(equality)],[267,19]),
[iquote('0:Res:267.10,19.0')] ).
cnf(551,plain,
( ~ intruder_message(at)
| ~ a_nonce(u)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ intruder_message(u)
| ~ intruder_message(x)
| message(sent(t,b,triple(encrypt(quadruple(a,u,generate_key(u),x),bt),encrypt(triple(b,generate_key(u),x),at),v))) ),
inference(obv,[status(thm),theory(equality)],[550]),
[iquote('0:Obv:550.0')] ).
cnf(546,plain,
( ~ a_nonce(u)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ intruder_message(u)
| ~ intruder_message(x)
| ~ intruder_holds(key(at,w))
| message(sent(t,b,triple(encrypt(quadruple(a,u,generate_key(u),x),bt),encrypt(triple(b,generate_key(u),x),at),v))) ),
inference(ssi,[status(thm)],[545,1,78]),
[iquote('0:SSi:545.2,545.0,1.0,78.0,1.0,78.0')] ).
cnf(549,plain,
( ~ intruder_message(bt)
| ~ a_nonce(u)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ intruder_message(u)
| ~ intruder_message(x)
| message(sent(t,a,triple(encrypt(quadruple(b,u,generate_key(u),x),at),encrypt(triple(a,generate_key(u),x),bt),v))) ),
inference(obv,[status(thm),theory(equality)],[548]),
[iquote('0:Obv:548.0')] ).
cnf(534,plain,
( ~ a_nonce(u)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ intruder_message(u)
| ~ intruder_message(x)
| ~ intruder_holds(key(bt,w))
| message(sent(t,a,triple(encrypt(quadruple(b,u,generate_key(u),x),at),encrypt(triple(a,generate_key(u),x),bt),v))) ),
inference(ssi,[status(thm)],[531,2,111]),
[iquote('0:SSi:531.2,531.0,2.0,111.0,2.0,111.0')] ).
cnf(415,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ party_of_protocol(x)
| ~ intruder_message(v)
| ~ intruder_message(y)
| ~ t_holds(key(z,u))
| ~ intruder_holds(key(z,x))
| message(sent(t,b,triple(encrypt(quadruple(u,v,generate_key(v),y),bt),encrypt(triple(b,generate_key(v),y),z),w))) ),
inference(ssi,[status(thm)],[412,2,111]),
[iquote('0:SSi:412.5,2.0,111.0')] ).
cnf(543,plain,
( ~ intruder_message(at)
| ~ a_nonce(u)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ intruder_message(u)
| ~ intruder_message(x)
| message(sent(t,a,triple(encrypt(quadruple(a,u,generate_key(u),x),at),encrypt(triple(a,generate_key(u),x),at),v))) ),
inference(obv,[status(thm),theory(equality)],[542]),
[iquote('0:Obv:542.0')] ).
cnf(533,plain,
( ~ a_nonce(u)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ intruder_message(u)
| ~ intruder_message(x)
| ~ intruder_holds(key(at,w))
| message(sent(t,a,triple(encrypt(quadruple(a,u,generate_key(u),x),at),encrypt(triple(a,generate_key(u),x),at),v))) ),
inference(ssi,[status(thm)],[532,1,78]),
[iquote('0:SSi:532.2,532.0,1.0,78.0,1.0,78.0')] ).
cnf(519,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ intruder_message(triple(a,generate_key(u),generate_expiration_time(v)))
| ~ intruder_message(bt)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_stored(pair(b,u))
| ~ b_stored(pair(a,v))
| b_holds(key(generate_key(u),a)) ),
inference(sor,[status(thm)],[480,145]),
[iquote('0:SoR:480.0,145.2')] ).
cnf(506,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(u)
| ~ party_of_protocol(v)
| ~ a_stored(pair(b,u))
| ~ t_holds(key(at,v))
| intruder_message(pair(encrypt(triple(v,generate_key(u),generate_expiration_time(u)),bt),encrypt(generate_b_nonce(u),generate_key(u)))) ),
inference(res,[status(thm),theory(equality)],[310,19]),
[iquote('0:Res:310.7,19.0')] ).
cnf(414,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ party_of_protocol(x)
| ~ intruder_message(v)
| ~ intruder_message(y)
| ~ t_holds(key(z,u))
| ~ intruder_holds(key(z,x))
| message(sent(t,a,triple(encrypt(quadruple(u,v,generate_key(v),y),at),encrypt(triple(a,generate_key(v),y),z),w))) ),
inference(ssi,[status(thm)],[413,1,78]),
[iquote('0:SSi:413.5,1.0,78.0')] ).
cnf(528,plain,
( ~ a_nonce(u)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(generate_expiration_time(v))
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ a_stored(pair(b,u))
| ~ b_stored(pair(a,v))
| b_holds(key(generate_key(u),a)) ),
inference(sor,[status(thm)],[527,145]),
[iquote('0:SoR:527.1,145.2')] ).
cnf(530,plain,
( ~ a_nonce(u)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ a_stored(pair(b,u))
| b_holds(key(generate_key(u),a)) ),
inference(mrr,[status(thm)],[529,88]),
[iquote('0:MRR:529.5,88.0')] ).
cnf(527,plain,
( ~ a_nonce(u)
| ~ intruder_message(generate_b_nonce(v))
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(generate_expiration_time(v))
| ~ a_stored(pair(b,u))
| ~ b_stored(pair(a,v))
| b_holds(key(generate_key(u),a)) ),
inference(mrr,[status(thm)],[526,13]),
[iquote('0:MRR:526.5,13.0')] ).
cnf(394,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(v)
| ~ intruder_message(y)
| ~ t_holds(key(x,u))
| ~ a_stored(pair(u,v))
| message(sent(a,u,pair(encrypt(triple(a,generate_key(v),y),x),encrypt(w,generate_key(v))))) ),
inference(mrr,[status(thm)],[393,12]),
[iquote('0:MRR:393.7,12.0')] ).
cnf(521,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ intruder_message(triple(a,generate_key(u),generate_expiration_time(an_a_nonce)))
| ~ intruder_message(bt)
| ~ a_stored(pair(b,u))
| b_holds(key(generate_key(u),a)) ),
inference(mrr,[status(thm)],[520,88]),
[iquote('0:MRR:520.6,88.0')] ).
cnf(480,plain,
( ~ intruder_message(generate_b_nonce(u))
| ~ a_nonce(v)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ intruder_message(triple(a,generate_key(v),generate_expiration_time(u)))
| ~ intruder_message(bt)
| ~ a_stored(pair(b,v))
| ~ b_stored(pair(a,u))
| b_holds(key(generate_key(v),a)) ),
inference(sor,[status(thm)],[422,92]),
[iquote('0:SoR:422.0,92.2')] ).
cnf(510,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ party_of_protocol(w)
| ~ a_stored(pair(w,an_a_nonce))
| ~ t_holds(key(bt,w))
| message(sent(a,w,pair(u,encrypt(v,generate_key(an_a_nonce))))) ),
inference(mrr,[status(thm)],[507,12]),
[iquote('0:MRR:507.6,12.0')] ).
cnf(501,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ t_holds(key(v,a))
| ~ t_holds(key(bt,u))
| intruder_message(encrypt(quadruple(u,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),v)) ),
inference(con,[status(thm)],[497]),
[iquote('0:Con:497.2')] ).
cnf(310,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(u)
| ~ party_of_protocol(v)
| ~ a_stored(pair(b,u))
| ~ t_holds(key(at,v))
| message(sent(a,b,pair(encrypt(triple(v,generate_key(u),generate_expiration_time(u)),bt),encrypt(generate_b_nonce(u),generate_key(u))))) ),
inference(sor,[status(thm)],[123,249]),
[iquote('0:SoR:123.0,249.6')] ).
cnf(357,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ t_holds(key(w,a))
| ~ t_holds(key(bt,u))
| intruder_message(triple(encrypt(quadruple(u,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),w),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),v)) ),
inference(res,[status(thm),theory(equality)],[201,19]),
[iquote('0:Res:201.5,19.0')] ).
cnf(422,plain,
( ~ intruder_message(encrypt(triple(a,generate_key(u),generate_expiration_time(v)),bt))
| ~ intruder_message(generate_b_nonce(v))
| ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ a_stored(pair(b,u))
| ~ b_stored(pair(a,v))
| b_holds(key(generate_key(u),a)) ),
inference(ssi,[status(thm)],[419,8]),
[iquote('0:SSi:419.5,8.0')] ).
cnf(307,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(bt)
| ~ a_nonce(v)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(v))
| ~ intruder_message(generate_expiration_time(v))
| ~ a_stored(pair(b,v))
| b_holds(key(generate_key(v),u)) ),
inference(mrr,[status(thm)],[306,100]),
[iquote('0:MRR:306.8,100.4')] ).
cnf(469,plain,
( ~ intruder_message(u)
| intruder_message(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(u,generate_key(an_a_nonce)))) ),
inference(mrr,[status(thm)],[468,10]),
[iquote('0:MRR:468.1,10.0')] ).
cnf(295,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ fresh_to_b(x)
| ~ party_of_protocol(y)
| ~ t_holds(key(z,b))
| ~ t_holds(key(x1,u))
| ~ intruder_holds(key(x1,w))
| message(sent(t,b,triple(encrypt(quadruple(u,generate_b_nonce(x),generate_key(generate_b_nonce(x)),encrypt(triple(y,x,generate_expiration_time(x)),bt)),z),encrypt(triple(b,generate_key(generate_b_nonce(x)),encrypt(triple(y,x,generate_expiration_time(x)),bt)),x1),v))) ),
inference(ssi,[status(thm)],[290,7,145]),
[iquote('0:SSi:290.1,7.2,145.0')] ).
cnf(362,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ t_holds(key(bt,u))
| ~ a_stored(pair(u,an_a_nonce))
| message(sent(a,u,pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(v,generate_key(an_a_nonce))))) ),
inference(mrr,[status(thm)],[358,12]),
[iquote('0:MRR:358.3,12.0')] ).
cnf(455,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(u)
| ~ party_of_protocol(v)
| ~ party_of_protocol(w)
| ~ t_holds(key(x,v))
| ~ intruder_holds(key(generate_key(u),w))
| b_holds(key(generate_key(u),v)) ),
inference(ssi,[status(thm)],[453,7,145]),
[iquote('0:SSi:453.5,7.2,145.0')] ).
cnf(454,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(u)
| ~ party_of_protocol(v)
| ~ intruder_message(generate_key(u))
| ~ t_holds(key(w,v))
| b_holds(key(generate_key(u),v)) ),
inference(ssi,[status(thm)],[452,7,145]),
[iquote('0:SSi:452.5,7.2,145.0')] ).
cnf(269,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ fresh_to_b(x)
| ~ party_of_protocol(y)
| ~ t_holds(key(z,b))
| ~ t_holds(key(w,u))
| message(sent(t,b,triple(encrypt(quadruple(u,generate_b_nonce(x),generate_key(generate_b_nonce(x)),encrypt(triple(y,x,generate_expiration_time(x)),bt)),z),encrypt(triple(b,generate_key(generate_b_nonce(x)),encrypt(triple(y,x,generate_expiration_time(x)),bt)),w),v))) ),
inference(ssi,[status(thm)],[264,7,145]),
[iquote('0:SSi:264.1,7.2,145.0')] ).
cnf(331,plain,
( ~ intruder_message(encrypt(generate_b_nonce(u),generate_key(u)))
| ~ a_nonce(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(u)
| ~ party_of_protocol(v)
| ~ t_holds(key(w,v))
| b_holds(key(generate_key(u),v)) ),
inference(mrr,[status(thm)],[330,100]),
[iquote('0:MRR:330.6,100.4')] ).
cnf(447,plain,
( ~ a_nonce(u)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ a_stored(pair(b,u))
| a_holds(key(generate_key(u),b)) ),
inference(ssi,[status(thm)],[444,2,111]),
[iquote('0:SSi:444.2,444.0,2.0,111.0,2.0,111.0')] ).
cnf(446,plain,
( ~ a_nonce(u)
| ~ intruder_message(at)
| ~ intruder_message(u)
| ~ a_stored(pair(a,u))
| a_holds(key(generate_key(u),a)) ),
inference(ssi,[status(thm)],[445,1,78]),
[iquote('0:SSi:445.2,445.0,1.0,78.0,1.0,78.0')] ).
cnf(392,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(v)
| ~ t_holds(key(w,u))
| ~ a_stored(pair(u,v))
| a_holds(key(generate_key(v),u)) ),
inference(mrr,[status(thm)],[391,12]),
[iquote('0:MRR:391.5,12.0')] ).
cnf(294,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ t_holds(key(x,b))
| ~ t_holds(key(y,u))
| ~ intruder_holds(key(y,w))
| message(sent(t,b,triple(encrypt(quadruple(u,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),x),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),y),v))) ),
inference(ssi,[status(thm)],[291,7,3,5,79,145]),
[iquote('0:SSi:291.1,7.0,3.0,5.0,79.2,145.0,3.0,5.0,79.0')] ).
cnf(429,plain,
( ~ intruder_message(u)
| ~ a_nonce(v)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ a_stored(pair(b,v))
| intruder_message(encrypt(u,generate_key(v))) ),
inference(con,[status(thm)],[428]),
[iquote('0:Con:428.0')] ).
cnf(420,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ a_nonce(w)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ a_stored(pair(b,w))
| intruder_message(pair(u,encrypt(v,generate_key(w)))) ),
inference(res,[status(thm),theory(equality)],[407,19]),
[iquote('0:Res:407.6,19.0')] ).
cnf(407,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ a_nonce(w)
| ~ intruder_message(w)
| ~ fresh_to_b(w)
| ~ a_stored(pair(b,w))
| message(sent(a,b,pair(u,encrypt(v,generate_key(w))))) ),
inference(sor,[status(thm)],[137,405]),
[iquote('0:SoR:137.0,405.3')] ).
cnf(406,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ a_nonce(u)
| intruder_message(encrypt(quadruple(b,u,generate_key(u),generate_expiration_time(u)),bt)) ),
inference(ssi,[status(thm)],[403,2,111]),
[iquote('0:SSi:403.2,403.0,2.0,111.0,2.0,111.0')] ).
cnf(293,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ party_of_protocol(x)
| ~ intruder_message(y)
| ~ intruder_message(v)
| ~ intruder_message(z)
| ~ t_holds(key(x1,y))
| ~ t_holds(key(x2,u))
| ~ intruder_holds(key(x2,x))
| message(sent(t,y,triple(encrypt(quadruple(u,v,generate_key(v),z),x1),encrypt(triple(y,generate_key(v),z),x2),w))) ),
inference(sor,[status(thm)],[200,29]),
[iquote('0:SoR:200.4,29.3')] ).
cnf(410,plain,
( ~ party_of_protocol(u)
| ~ intruder_holds(key(at,u))
| intruder_message(at) ),
inference(ems,[status(thm)],[409,3,79,5]),
[iquote('0:EmS:409.0,409.1,409.2,3.0,79.0,5.0')] ).
cnf(405,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ a_nonce(u)
| intruder_message(encrypt(quadruple(b,u,generate_key(u),generate_expiration_time(u)),at)) ),
inference(ssi,[status(thm)],[404,1,78]),
[iquote('0:SSi:404.2,404.0,1.0,78.0,1.0,78.0')] ).
cnf(312,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ t_holds(key(w,u))
| intruder_message(encrypt(quadruple(b,v,generate_key(v),generate_expiration_time(v)),w)) ),
inference(res,[status(thm),theory(equality)],[249,20]),
[iquote('0:Res:249.6,20.0')] ).
cnf(268,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ t_holds(key(x,b))
| ~ t_holds(key(w,u))
| message(sent(t,b,triple(encrypt(quadruple(u,generate_b_nonce(an_a_nonce),generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),x),encrypt(triple(b,generate_key(generate_b_nonce(an_a_nonce)),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),w),v))) ),
inference(ssi,[status(thm)],[265,7,3,5,79,145]),
[iquote('0:SSi:265.1,7.0,3.0,5.0,79.2,145.0,3.0,5.0,79.0')] ).
cnf(333,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ fresh_to_b(u)
| ~ party_of_protocol(v)
| ~ a_stored(pair(b,u))
| ~ t_holds(key(w,v))
| b_holds(key(generate_key(u),v)) ),
inference(mrr,[status(thm)],[332,100]),
[iquote('0:MRR:332.5,100.4')] ).
cnf(385,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ party_of_protocol(v)
| ~ b_stored(pair(b,u))
| ~ intruder_holds(key(generate_key(u),v))
| b_holds(key(generate_key(u),b)) ),
inference(ssi,[status(thm)],[383,7,145]),
[iquote('0:SSi:383.3,7.2,145.0')] ).
cnf(377,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ party_of_protocol(v)
| ~ b_stored(pair(a,u))
| ~ intruder_holds(key(generate_key(u),v))
| b_holds(key(generate_key(u),a)) ),
inference(ssi,[status(thm)],[375,7,145]),
[iquote('0:SSi:375.3,7.2,145.0')] ).
cnf(384,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ intruder_message(generate_key(u))
| ~ b_stored(pair(b,u))
| b_holds(key(generate_key(u),b)) ),
inference(ssi,[status(thm)],[382,7,145]),
[iquote('0:SSi:382.3,7.2,145.0')] ).
cnf(267,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ intruder_message(v)
| ~ intruder_message(z)
| ~ t_holds(key(x1,y))
| ~ t_holds(key(x,u))
| message(sent(t,y,triple(encrypt(quadruple(u,v,generate_key(v),z),x1),encrypt(triple(y,generate_key(v),z),x),w))) ),
inference(sor,[status(thm)],[199,29]),
[iquote('0:SoR:199.4,29.3')] ).
cnf(354,plain,
( ~ intruder_message(encrypt(generate_b_nonce(u),generate_key(u)))
| ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ b_stored(pair(b,u))
| b_holds(key(generate_key(u),b)) ),
inference(ssi,[status(thm)],[345,8,2,111]),
[iquote('0:SSi:345.1,345.0,8.0,2.0,111.0')] ).
cnf(376,plain,
( ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ intruder_message(generate_key(u))
| ~ b_stored(pair(a,u))
| b_holds(key(generate_key(u),a)) ),
inference(ssi,[status(thm)],[374,7,145]),
[iquote('0:SSi:374.3,7.2,145.0')] ).
cnf(343,plain,
( ~ intruder_message(encrypt(generate_b_nonce(u),generate_key(u)))
| ~ a_nonce(u)
| ~ intruder_message(u)
| ~ fresh_to_b(u)
| ~ b_stored(pair(a,u))
| b_holds(key(generate_key(u),a)) ),
inference(ssi,[status(thm)],[335,8,1,78]),
[iquote('0:SSi:335.1,335.0,8.0,1.0,78.0')] ).
cnf(242,plain,
( ~ party_of_protocol(u)
| ~ a_key(v)
| ~ intruder_message(triple(u,v,generate_expiration_time(w)))
| ~ party_of_protocol(x)
| ~ intruder_message(generate_b_nonce(w))
| ~ party_of_protocol(y)
| ~ b_stored(pair(u,w))
| ~ intruder_holds(key(bt,x))
| ~ intruder_holds(key(v,y))
| b_holds(key(v,u)) ),
inference(sor,[status(thm)],[174,33]),
[iquote('0:SoR:174.2,33.3')] ).
cnf(369,plain,
b_holds(key(generate_key(an_a_nonce),b)),
inference(ssi,[status(thm)],[367,2,111]),
[iquote('0:SSi:367.1,367.0,2.0,111.0,2.0,111.0')] ).
cnf(366,plain,
( ~ intruder_message(u)
| ~ party_of_protocol(u)
| ~ t_holds(key(v,u))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(ssi,[status(thm)],[365,3,5,79]),
[iquote('0:SSi:365.1,365.0,3.0,5.0,79.0,3.0,5.0,79.0')] ).
cnf(361,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ t_holds(key(bt,u))
| ~ a_stored(pair(u,an_a_nonce))
| a_holds(key(generate_key(an_a_nonce),u)) ),
inference(mrr,[status(thm)],[360,12]),
[iquote('0:MRR:360.2,12.0')] ).
cnf(201,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ t_holds(key(w,a))
| ~ t_holds(key(bt,u))
| message(sent(t,a,triple(encrypt(quadruple(u,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),w),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),v))) ),
inference(ssi,[status(thm)],[198,3,5,79]),
[iquote('0:SSi:198.1,3.0,5.0,79.0')] ).
cnf(324,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ a_nonce(u)
| intruder_message(encrypt(triple(b,generate_key(u),generate_expiration_time(u)),bt)) ),
inference(ssi,[status(thm)],[321,2,111]),
[iquote('0:SSi:321.2,321.0,2.0,111.0,2.0,111.0')] ).
cnf(323,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ a_nonce(u)
| intruder_message(encrypt(triple(a,generate_key(u),generate_expiration_time(u)),bt)) ),
inference(ssi,[status(thm)],[322,1,78]),
[iquote('0:SSi:322.2,322.0,1.0,78.0,1.0,78.0')] ).
cnf(313,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ t_holds(key(w,u))
| intruder_message(encrypt(triple(u,generate_key(v),generate_expiration_time(v)),bt)) ),
inference(res,[status(thm),theory(equality)],[249,21]),
[iquote('0:Res:249.6,21.0')] ).
cnf(249,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ t_holds(key(w,u))
| intruder_message(triple(encrypt(quadruple(b,v,generate_key(v),generate_expiration_time(v)),w),encrypt(triple(u,generate_key(v),generate_expiration_time(v)),bt),generate_b_nonce(v))) ),
inference(res,[status(thm),theory(equality)],[140,19]),
[iquote('0:Res:140.6,19.0')] ).
cnf(275,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(triple(u,generate_key(v),generate_expiration_time(v)))
| ~ intruder_message(bt)
| ~ a_nonce(v)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ b_stored(pair(u,v))
| ~ a_stored(pair(b,v))
| b_holds(key(generate_key(v),u)) ),
inference(ssi,[status(thm)],[271,8]),
[iquote('0:SSi:271.1,8.0')] ).
cnf(305,plain,
( ~ party_of_protocol(u)
| ~ a_key(v)
| ~ party_of_protocol(w)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(generate_expiration_time(x))
| ~ fresh_to_b(x)
| ~ intruder_message(x)
| ~ intruder_holds(key(bt,w))
| b_holds(key(v,u)) ),
inference(mrr,[status(thm)],[303,100]),
[iquote('0:MRR:303.8,100.4')] ).
cnf(304,plain,
( ~ party_of_protocol(u)
| ~ a_key(v)
| ~ party_of_protocol(w)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ b_stored(pair(u,an_a_nonce))
| ~ intruder_holds(key(bt,w))
| b_holds(key(v,u)) ),
inference(sor,[status(thm)],[302,112]),
[iquote('0:SoR:302.3,112.0')] ).
cnf(302,plain,
( ~ party_of_protocol(u)
| ~ a_key(v)
| ~ party_of_protocol(w)
| ~ intruder_message(generate_b_nonce(x))
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(generate_expiration_time(x))
| ~ b_stored(pair(u,x))
| ~ intruder_holds(key(bt,w))
| b_holds(key(v,u)) ),
inference(obv,[status(thm),theory(equality)],[301]),
[iquote('0:Obv:301.4')] ).
cnf(241,plain,
( ~ party_of_protocol(u)
| ~ a_key(v)
| ~ intruder_message(triple(u,v,generate_expiration_time(w)))
| ~ party_of_protocol(x)
| ~ intruder_message(generate_b_nonce(w))
| ~ intruder_message(v)
| ~ b_stored(pair(u,w))
| ~ intruder_holds(key(bt,x))
| b_holds(key(v,u)) ),
inference(sor,[status(thm)],[174,92]),
[iquote('0:SoR:174.2,92.2')] ).
cnf(300,plain,
( ~ intruder_message(at)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ intruder_message(x)
| message(sent(a,b,pair(u,encrypt(v,x)))) ),
inference(obv,[status(thm),theory(equality)],[299]),
[iquote('0:Obv:299.0')] ).
cnf(298,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ intruder_message(x)
| ~ intruder_holds(key(at,w))
| message(sent(a,b,pair(u,encrypt(v,x)))) ),
inference(ssi,[status(thm)],[297,3,5,79,2,111]),
[iquote('0:SSi:297.4,297.3,3.0,5.0,79.0,2.0,111.0')] ).
cnf(236,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ intruder_message(z)
| ~ a_stored(pair(x,y))
| ~ intruder_holds(key(at,w))
| message(sent(a,x,pair(u,encrypt(v,z)))) ),
inference(con,[status(thm)],[235]),
[iquote('0:Con:235.6')] ).
cnf(230,plain,
( ~ party_of_protocol(u)
| ~ a_key(v)
| ~ intruder_message(triple(u,v,generate_expiration_time(w)))
| ~ intruder_message(bt)
| ~ intruder_message(generate_b_nonce(w))
| ~ party_of_protocol(x)
| ~ b_stored(pair(u,w))
| ~ intruder_holds(key(v,x))
| b_holds(key(v,u)) ),
inference(sor,[status(thm)],[173,33]),
[iquote('0:SoR:173.2,33.3')] ).
cnf(200,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(triple(x,v,y))
| ~ party_of_protocol(z)
| ~ t_holds(key(x1,x))
| ~ t_holds(key(x2,u))
| ~ intruder_holds(key(x2,z))
| message(sent(t,x,triple(encrypt(quadruple(u,v,generate_key(v),y),x1),encrypt(triple(x,generate_key(v),y),x2),w))) ),
inference(sor,[status(thm)],[150,33]),
[iquote('0:SoR:150.4,33.3')] ).
cnf(274,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(encrypt(triple(u,generate_key(v),generate_expiration_time(v)),bt))
| ~ a_nonce(v)
| ~ intruder_message(v)
| ~ fresh_to_b(v)
| ~ b_stored(pair(u,v))
| ~ a_stored(pair(b,v))
| b_holds(key(generate_key(v),u)) ),
inference(ssi,[status(thm)],[272,8]),
[iquote('0:SSi:272.1,8.0')] ).
cnf(273,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ a_nonce(u)
| ~ party_of_protocol(v)
| ~ a_stored(pair(b,u))
| ~ intruder_holds(key(generate_key(u),v))
| intruder_message(generate_key(u)) ),
inference(res,[status(thm),theory(equality)],[263,32]),
[iquote('0:Res:263.4,32.1')] ).
cnf(263,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ a_nonce(u)
| ~ a_stored(pair(b,u))
| intruder_message(encrypt(generate_b_nonce(u),generate_key(u))) ),
inference(res,[status(thm),theory(equality)],[257,18]),
[iquote('0:Res:257.4,18.0')] ).
cnf(199,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(triple(x,v,y))
| ~ intruder_message(z)
| ~ t_holds(key(x1,x))
| ~ t_holds(key(z,u))
| message(sent(t,x,triple(encrypt(quadruple(u,v,generate_key(v),y),x1),encrypt(triple(x,generate_key(v),y),z),w))) ),
inference(sor,[status(thm)],[150,92]),
[iquote('0:SoR:150.4,92.2')] ).
cnf(257,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ a_nonce(u)
| ~ a_stored(pair(b,u))
| intruder_message(pair(encrypt(triple(a,generate_key(u),generate_expiration_time(u)),bt),encrypt(generate_b_nonce(u),generate_key(u)))) ),
inference(res,[status(thm),theory(equality)],[255,19]),
[iquote('0:Res:255.4,19.0')] ).
cnf(258,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ a_nonce(u)
| ~ a_stored(pair(b,u))
| ~ b_stored(pair(a,u))
| b_holds(key(generate_key(u),a)) ),
inference(ssi,[status(thm)],[256,8]),
[iquote('0:SSi:256.3,8.0')] ).
cnf(255,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ a_nonce(u)
| ~ a_stored(pair(b,u))
| message(sent(a,b,pair(encrypt(triple(a,generate_key(u),generate_expiration_time(u)),bt),encrypt(generate_b_nonce(u),generate_key(u))))) ),
inference(mrr,[status(thm)],[254,12]),
[iquote('0:MRR:254.3,12.0')] ).
cnf(253,plain,
( ~ fresh_to_b(u)
| ~ intruder_message(u)
| ~ a_nonce(u)
| ~ a_stored(pair(b,u))
| a_holds(key(generate_key(u),b)) ),
inference(mrr,[status(thm)],[252,12]),
[iquote('0:MRR:252.3,12.0')] ).
cnf(140,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ a_nonce(v)
| ~ t_holds(key(w,u))
| message(sent(t,u,triple(encrypt(quadruple(b,v,generate_key(v),generate_expiration_time(v)),w),encrypt(triple(u,generate_key(v),generate_expiration_time(v)),bt),generate_b_nonce(v)))) ),
inference(mrr,[status(thm)],[139,13]),
[iquote('0:MRR:139.6,13.0')] ).
cnf(244,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(generate_b_nonce(w))
| ~ intruder_message(u)
| ~ intruder_message(generate_key(an_a_nonce))
| ~ intruder_message(generate_expiration_time(w))
| ~ b_stored(pair(u,w))
| ~ intruder_holds(key(bt,v))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(sor,[status(thm)],[243,29]),
[iquote('0:SoR:243.1,29.3')] ).
cnf(246,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ party_of_protocol(w)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(an_a_nonce))
| ~ intruder_message(generate_expiration_time(v))
| ~ intruder_holds(key(bt,w))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(mrr,[status(thm)],[245,100]),
[iquote('0:MRR:245.7,100.4')] ).
cnf(224,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ intruder_message(triple(u,generate_key(an_a_nonce),generate_expiration_time(v)))
| ~ party_of_protocol(w)
| ~ b_stored(pair(u,v))
| ~ intruder_holds(key(bt,w))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(sor,[status(thm)],[212,33]),
[iquote('0:SoR:212.1,33.3')] ).
cnf(243,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(triple(u,generate_key(an_a_nonce),generate_expiration_time(v)))
| ~ party_of_protocol(w)
| ~ intruder_message(generate_b_nonce(v))
| ~ b_stored(pair(u,v))
| ~ intruder_holds(key(bt,w))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(ssi,[status(thm)],[239,8,3,5,79]),
[iquote('0:SSi:239.1,8.0,3.0,5.0,79.0')] ).
cnf(174,plain,
( ~ party_of_protocol(u)
| ~ a_key(v)
| ~ intruder_message(encrypt(generate_b_nonce(w),v))
| ~ intruder_message(triple(u,v,generate_expiration_time(w)))
| ~ party_of_protocol(x)
| ~ b_stored(pair(u,w))
| ~ intruder_holds(key(bt,x))
| b_holds(key(v,u)) ),
inference(sor,[status(thm)],[141,33]),
[iquote('0:SoR:141.2,33.3')] ).
cnf(238,plain,
( ~ party_of_protocol(u)
| ~ a_key(v)
| ~ intruder_message(bt)
| ~ intruder_message(generate_b_nonce(w))
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(generate_expiration_time(w))
| ~ b_stored(pair(u,w))
| b_holds(key(v,u)) ),
inference(obv,[status(thm),theory(equality)],[237]),
[iquote('0:Obv:237.4')] ).
cnf(229,plain,
( ~ party_of_protocol(u)
| ~ a_key(v)
| ~ intruder_message(triple(u,v,generate_expiration_time(w)))
| ~ intruder_message(bt)
| ~ intruder_message(generate_b_nonce(w))
| ~ intruder_message(v)
| ~ b_stored(pair(u,w))
| b_holds(key(v,u)) ),
inference(sor,[status(thm)],[173,92]),
[iquote('0:SoR:173.2,92.2')] ).
cnf(218,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(at)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ intruder_message(y)
| ~ a_stored(pair(w,x))
| message(sent(a,w,pair(u,encrypt(v,y)))) ),
inference(con,[status(thm)],[217]),
[iquote('0:Con:217.6')] ).
cnf(220,plain,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(an_a_nonce))
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ b_stored(pair(u,an_a_nonce))
| ~ intruder_holds(key(bt,v))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(sor,[status(thm)],[216,29]),
[iquote('0:SoR:216.1,29.3')] ).
cnf(161,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(quadruple(w,x,y,z))
| ~ party_of_protocol(x1)
| ~ a_stored(pair(w,x))
| ~ intruder_holds(key(at,x1))
| message(sent(a,w,pair(u,encrypt(v,y)))) ),
inference(sor,[status(thm)],[137,33]),
[iquote('0:SoR:137.0,33.3')] ).
cnf(232,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(bt)
| ~ intruder_message(generate_b_nonce(v))
| ~ intruder_message(u)
| ~ intruder_message(generate_key(an_a_nonce))
| ~ intruder_message(generate_expiration_time(v))
| ~ b_stored(pair(u,v))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(sor,[status(thm)],[231,29]),
[iquote('0:SoR:231.1,29.3')] ).
cnf(234,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(an_a_nonce))
| ~ intruder_message(generate_expiration_time(v))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(mrr,[status(thm)],[233,100]),
[iquote('0:MRR:233.7,100.4')] ).
cnf(223,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ intruder_message(triple(u,generate_key(an_a_nonce),generate_expiration_time(v)))
| ~ intruder_message(bt)
| ~ b_stored(pair(u,v))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(sor,[status(thm)],[212,92]),
[iquote('0:SoR:212.1,92.2')] ).
cnf(231,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(triple(u,generate_key(an_a_nonce),generate_expiration_time(v)))
| ~ intruder_message(bt)
| ~ intruder_message(generate_b_nonce(v))
| ~ b_stored(pair(u,v))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(ssi,[status(thm)],[227,8,3,5,79]),
[iquote('0:SSi:227.1,8.0,3.0,5.0,79.0')] ).
cnf(173,plain,
( ~ party_of_protocol(u)
| ~ a_key(v)
| ~ intruder_message(encrypt(generate_b_nonce(w),v))
| ~ intruder_message(triple(u,v,generate_expiration_time(w)))
| ~ intruder_message(bt)
| ~ b_stored(pair(u,w))
| b_holds(key(v,u)) ),
inference(sor,[status(thm)],[141,92]),
[iquote('0:SoR:141.2,92.2')] ).
cnf(212,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(encrypt(triple(u,generate_key(an_a_nonce),generate_expiration_time(v)),bt))
| ~ fresh_to_b(v)
| ~ intruder_message(v)
| ~ b_stored(pair(u,v))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(sor,[status(thm)],[208,145]),
[iquote('0:SoR:208.1,145.2')] ).
cnf(216,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(triple(u,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)))
| ~ party_of_protocol(v)
| ~ b_stored(pair(u,an_a_nonce))
| ~ intruder_holds(key(bt,v))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(sor,[status(thm)],[213,33]),
[iquote('0:SoR:213.1,33.3')] ).
cnf(219,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(bt)
| ~ intruder_message(u)
| ~ intruder_message(generate_key(an_a_nonce))
| ~ intruder_message(generate_expiration_time(an_a_nonce))
| ~ b_stored(pair(u,an_a_nonce))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(sor,[status(thm)],[215,29]),
[iquote('0:SoR:215.1,29.3')] ).
cnf(215,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(triple(u,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)))
| ~ intruder_message(bt)
| ~ b_stored(pair(u,an_a_nonce))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(sor,[status(thm)],[213,92]),
[iquote('0:SoR:213.1,92.2')] ).
cnf(160,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(quadruple(w,x,y,z))
| ~ intruder_message(at)
| ~ a_stored(pair(w,x))
| message(sent(a,w,pair(u,encrypt(v,y)))) ),
inference(sor,[status(thm)],[137,92]),
[iquote('0:SoR:137.0,92.2')] ).
cnf(213,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(encrypt(triple(u,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt))
| ~ b_stored(pair(u,an_a_nonce))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(sor,[status(thm)],[208,112]),
[iquote('0:SoR:208.1,112.0')] ).
cnf(208,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(generate_b_nonce(v))
| ~ intruder_message(encrypt(triple(u,generate_key(an_a_nonce),generate_expiration_time(v)),bt))
| ~ b_stored(pair(u,v))
| b_holds(key(generate_key(an_a_nonce),u)) ),
inference(ssi,[status(thm)],[204,8,3,5,79]),
[iquote('0:SSi:204.1,8.0,3.0,5.0,79.0')] ).
cnf(207,plain,
( ~ intruder_message(u)
| intruder_message(encrypt(u,generate_key(an_a_nonce))) ),
inference(con,[status(thm)],[206]),
[iquote('0:Con:206.0')] ).
cnf(193,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| intruder_message(pair(u,encrypt(v,generate_key(an_a_nonce)))) ),
inference(res,[status(thm),theory(equality)],[188,19]),
[iquote('0:Res:188.2,19.0')] ).
cnf(150,plain,
( ~ party_of_protocol(u)
| ~ a_nonce(v)
| ~ intruder_message(u)
| ~ intruder_message(w)
| ~ intruder_message(encrypt(triple(x,v,y),z))
| ~ t_holds(key(x1,x))
| ~ t_holds(key(z,u))
| message(sent(t,x,triple(encrypt(quadruple(u,v,generate_key(v),y),x1),encrypt(triple(x,generate_key(v),y),z),w))) ),
inference(sor,[status(thm)],[134,29]),
[iquote('0:SoR:134.1,29.3')] ).
cnf(188,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| message(sent(a,b,pair(u,encrypt(v,generate_key(an_a_nonce))))) ),
inference(mrr,[status(thm)],[185,10,12]),
[iquote('0:MRR:185.2,185.3,10.0,12.0')] ).
cnf(187,plain,
( ~ party_of_protocol(u)
| ~ t_holds(key(v,a))
| ~ intruder_holds(key(v,u))
| intruder_message(v) ),
inference(res,[status(thm),theory(equality)],[182,32]),
[iquote('0:Res:182.1,32.1')] ).
cnf(182,plain,
( ~ t_holds(key(u,a))
| intruder_message(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),u)) ),
inference(res,[status(thm),theory(equality)],[151,20]),
[iquote('0:Res:151.1,20.0')] ).
cnf(151,plain,
( ~ t_holds(key(u,a))
| intruder_message(triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),u),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),generate_b_nonce(an_a_nonce))) ),
inference(res,[status(thm),theory(equality)],[133,19]),
[iquote('0:Res:133.1,19.0')] ).
cnf(141,plain,
( ~ party_of_protocol(u)
| ~ a_key(v)
| ~ intruder_message(encrypt(triple(u,v,generate_expiration_time(w)),bt))
| ~ intruder_message(encrypt(generate_b_nonce(w),v))
| ~ b_stored(pair(u,w))
| b_holds(key(v,u)) ),
inference(sor,[status(thm)],[115,27]),
[iquote('0:SoR:115.1,27.2')] ).
cnf(167,plain,
( ~ party_of_protocol(u)
| ~ intruder_holds(key(generate_key(an_a_nonce),u))
| intruder_message(generate_key(an_a_nonce)) ),
inference(res,[status(thm),theory(equality)],[166,32]),
[iquote('0:Res:166.0,32.1')] ).
cnf(165,plain,
intruder_message(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt)),
inference(res,[status(thm),theory(equality)],[157,17]),
[iquote('0:Res:157.0,17.0')] ).
cnf(166,plain,
intruder_message(encrypt(generate_b_nonce(an_a_nonce),generate_key(an_a_nonce))),
inference(res,[status(thm),theory(equality)],[157,18]),
[iquote('0:Res:157.0,18.0')] ).
cnf(157,plain,
intruder_message(pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(generate_b_nonce(an_a_nonce),generate_key(an_a_nonce)))),
inference(res,[status(thm),theory(equality)],[155,19]),
[iquote('0:Res:155.0,19.0')] ).
cnf(137,plain,
( ~ intruder_message(encrypt(quadruple(u,v,w,x),at))
| ~ intruder_message(y)
| ~ intruder_message(z)
| ~ a_stored(pair(u,v))
| message(sent(a,u,pair(y,encrypt(z,w)))) ),
inference(sor,[status(thm)],[123,29]),
[iquote('0:SoR:123.0,29.3')] ).
cnf(159,plain,
b_holds(key(generate_key(an_a_nonce),a)),
inference(mrr,[status(thm)],[158,88]),
[iquote('0:MRR:158.0,88.0')] ).
cnf(155,plain,
message(sent(a,b,pair(encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),encrypt(generate_b_nonce(an_a_nonce),generate_key(an_a_nonce))))),
inference(mrr,[status(thm)],[152,12,10]),
[iquote('0:MRR:152.0,152.1,12.0,10.0')] ).
cnf(154,plain,
a_holds(key(generate_key(an_a_nonce),b)),
inference(mrr,[status(thm)],[153,12,10]),
[iquote('0:MRR:153.0,153.1,12.0,10.0')] ).
cnf(133,plain,
( ~ t_holds(key(u,a))
| message(sent(t,a,triple(encrypt(quadruple(b,an_a_nonce,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),u),encrypt(triple(a,generate_key(an_a_nonce),generate_expiration_time(an_a_nonce)),bt),generate_b_nonce(an_a_nonce)))) ),
inference(mrr,[status(thm)],[132,13]),
[iquote('0:MRR:132.1,13.0')] ).
cnf(134,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(triple(u,v,encrypt(triple(w,x,y),z)))
| ~ a_nonce(x)
| ~ t_holds(key(x1,w))
| ~ t_holds(key(z,u))
| message(sent(t,w,triple(encrypt(quadruple(u,x,generate_key(x),y),x1),encrypt(triple(w,generate_key(x),y),z),v))) ),
inference(ssi,[status(thm)],[130,4]),
[iquote('0:SSi:130.0,4.0')] ).
cnf(144,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| intruder_message(encrypt(triple(u,v,generate_expiration_time(v)),bt)) ),
inference(res,[status(thm),theory(equality)],[138,22]),
[iquote('0:Res:138.4,22.0')] ).
cnf(145,plain,
( ~ intruder_message(u)
| ~ fresh_to_b(u)
| intruder_message(generate_b_nonce(u)) ),
inference(ems,[status(thm)],[143,2,111]),
[iquote('0:EmS:143.0,143.2,2.0,111.0')] ).
cnf(138,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| intruder_message(triple(b,generate_b_nonce(v),encrypt(triple(u,v,generate_expiration_time(v)),bt))) ),
inference(res,[status(thm),theory(equality)],[126,19]),
[iquote('0:Res:126.4,19.0')] ).
cnf(115,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(pair(encrypt(triple(u,v,generate_expiration_time(w)),bt),encrypt(generate_b_nonce(w),v)))
| ~ a_key(v)
| ~ b_stored(pair(u,w))
| b_holds(key(v,u)) ),
inference(ssi,[status(thm)],[114,2,111]),
[iquote('0:SSi:114.0,2.0,111.0')] ).
cnf(126,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| message(sent(b,t,triple(b,generate_b_nonce(v),encrypt(triple(u,v,generate_expiration_time(v)),bt)))) ),
inference(sor,[status(thm)],[109,27]),
[iquote('0:SoR:109.1,27.2')] ).
cnf(123,plain,
( ~ intruder_message(triple(encrypt(quadruple(u,v,w,x),at),y,z))
| ~ a_stored(pair(u,v))
| message(sent(a,u,pair(y,encrypt(z,w)))) ),
inference(ssi,[status(thm)],[122,4,1,78]),
[iquote('0:SSi:122.1,122.0,4.0,1.0,78.0')] ).
cnf(136,plain,
( ~ intruder_message(at)
| ~ party_of_protocol(u)
| ~ intruder_message(v)
| a_holds(key(v,b)) ),
inference(obv,[status(thm),theory(equality)],[135]),
[iquote('0:Obv:135.0')] ).
cnf(129,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(v)
| ~ intruder_holds(key(at,u))
| a_holds(key(v,b)) ),
inference(ssi,[status(thm)],[128,3,5,79,2,111]),
[iquote('0:SSi:128.2,128.1,3.0,5.0,79.0,2.0,111.0')] ).
cnf(39,axiom,
( ~ a_nonce(u)
| ~ t_holds(key(v,w))
| ~ t_holds(key(x,y))
| ~ message(sent(y,t,triple(y,z,encrypt(triple(w,u,x1),x))))
| message(sent(t,w,triple(encrypt(quadruple(y,u,generate_key(u),x1),v),encrypt(triple(w,generate_key(u),x1),x),z))) ),
file('SWV015+1.p',unknown),
[] ).
cnf(125,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| ~ a_stored(pair(v,w))
| ~ intruder_holds(key(at,u))
| a_holds(key(x,v)) ),
inference(con,[status(thm)],[124]),
[iquote('0:Con:124.4')] ).
cnf(109,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(pair(u,v))
| ~ fresh_to_b(v)
| message(sent(b,t,triple(b,generate_b_nonce(v),encrypt(triple(u,v,generate_expiration_time(v)),bt)))) ),
inference(ssi,[status(thm)],[107,2]),
[iquote('0:SSi:107.0,2.0')] ).
cnf(119,plain,
( ~ intruder_message(quadruple(u,v,w,x))
| ~ party_of_protocol(y)
| ~ a_stored(pair(u,v))
| ~ intruder_holds(key(at,y))
| a_holds(key(w,u)) ),
inference(sor,[status(thm)],[105,33]),
[iquote('0:SoR:105.0,33.3')] ).
cnf(121,plain,
( ~ intruder_message(at)
| ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ a_stored(pair(u,v))
| a_holds(key(w,u)) ),
inference(con,[status(thm)],[120]),
[iquote('0:Con:120.4')] ).
cnf(38,axiom,
( ~ a_stored(pair(u,v))
| ~ message(sent(t,a,triple(encrypt(quadruple(u,v,w,x),at),y,z)))
| message(sent(a,u,pair(y,encrypt(z,w)))) ),
file('SWV015+1.p',unknown),
[] ).
cnf(118,plain,
( ~ intruder_message(quadruple(u,v,w,x))
| ~ intruder_message(at)
| ~ a_stored(pair(u,v))
| a_holds(key(w,u)) ),
inference(sor,[status(thm)],[105,92]),
[iquote('0:SoR:105.0,92.2')] ).
cnf(105,plain,
( ~ intruder_message(encrypt(quadruple(u,v,w,x),at))
| ~ a_stored(pair(u,v))
| a_holds(key(w,u)) ),
inference(con,[status(thm)],[104]),
[iquote('0:Con:104.1')] ).
cnf(116,plain,
( ~ party_of_protocol(u)
| ~ intruder_holds(key(bt,u))
| intruder_message(bt) ),
inference(res,[status(thm),theory(equality)],[113,32]),
[iquote('0:Res:113.0,32.1')] ).
cnf(113,plain,
intruder_message(encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)),
inference(res,[status(thm),theory(equality)],[110,22]),
[iquote('0:Res:110.0,22.0')] ).
cnf(37,axiom,
( ~ a_key(u)
| ~ b_stored(pair(v,w))
| ~ message(sent(v,b,pair(encrypt(triple(v,u,generate_expiration_time(w)),bt),encrypt(generate_b_nonce(w),u))))
| b_holds(key(u,v)) ),
file('SWV015+1.p',unknown),
[] ).
cnf(112,plain,
intruder_message(generate_b_nonce(an_a_nonce)),
inference(res,[status(thm),theory(equality)],[110,21]),
[iquote('0:Res:110.0,21.0')] ).
cnf(111,plain,
intruder_message(b),
inference(res,[status(thm),theory(equality)],[110,20]),
[iquote('0:Res:110.0,20.0')] ).
cnf(110,plain,
intruder_message(triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt))),
inference(res,[status(thm),theory(equality)],[108,19]),
[iquote('0:Res:108.0,19.0')] ).
cnf(108,plain,
message(sent(b,t,triple(b,generate_b_nonce(an_a_nonce),encrypt(triple(a,an_a_nonce,generate_expiration_time(an_a_nonce)),bt)))),
inference(ssi,[status(thm)],[106,3,5,79]),
[iquote('0:SSi:106.0,3.0,5.0,79.0')] ).
cnf(36,axiom,
( ~ fresh_to_b(u)
| ~ message(sent(v,b,pair(v,u)))
| message(sent(b,t,triple(b,generate_b_nonce(u),encrypt(triple(v,u,generate_expiration_time(u)),bt)))) ),
file('SWV015+1.p',unknown),
[] ).
cnf(103,plain,
( ~ intruder_message(triple(encrypt(quadruple(u,v,w,x),at),y,z))
| ~ a_stored(pair(u,v))
| a_holds(key(w,u)) ),
inference(ssi,[status(thm)],[102,4,1,78]),
[iquote('0:SSi:102.1,102.0,4.0,1.0,78.0')] ).
cnf(35,axiom,
( ~ a_stored(pair(u,v))
| ~ message(sent(t,a,triple(encrypt(quadruple(u,v,w,x),at),y,z)))
| a_holds(key(w,u)) ),
file('SWV015+1.p',unknown),
[] ).
cnf(100,plain,
( ~ party_of_protocol(u)
| ~ fresh_to_b(v)
| ~ intruder_message(u)
| ~ intruder_message(v)
| b_stored(pair(u,v)) ),
inference(sor,[status(thm)],[89,27]),
[iquote('0:SoR:89.1,27.2')] ).
cnf(89,plain,
( ~ party_of_protocol(u)
| ~ intruder_message(pair(u,v))
| ~ fresh_to_b(v)
| b_stored(pair(u,v)) ),
inference(ssi,[status(thm)],[87,2]),
[iquote('0:SSi:87.0,2.0')] ).
cnf(34,axiom,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| ~ intruder_message(x)
| intruder_message(quadruple(x,w,v,u)) ),
file('SWV015+1.p',unknown),
[] ).
cnf(32,axiom,
( ~ party_of_protocol(u)
| ~ intruder_message(encrypt(v,w))
| ~ intruder_holds(key(w,u))
| intruder_message(w) ),
file('SWV015+1.p',unknown),
[] ).
cnf(92,plain,
( ~ intruder_message(u)
| ~ intruder_message(v)
| intruder_message(encrypt(v,u)) ),
inference(ems,[status(thm)],[91,1]),
[iquote('0:EmS:91.1,1.0')] ).
cnf(88,plain,
b_stored(pair(a,an_a_nonce)),
inference(ssi,[status(thm)],[86,3,5,79]),
[iquote('0:SSi:86.0,3.0,5.0,79.0')] ).
cnf(33,axiom,
( ~ party_of_protocol(u)
| ~ intruder_message(v)
| ~ intruder_holds(key(w,u))
| intruder_message(encrypt(v,w)) ),
file('SWV015+1.p',unknown),
[] ).
cnf(31,axiom,
( ~ fresh_to_b(u)
| ~ message(sent(v,b,pair(v,u)))
| b_stored(pair(v,u)) ),
file('SWV015+1.p',unknown),
[] ).
cnf(29,axiom,
( ~ intruder_message(u)
| ~ intruder_message(v)
| ~ intruder_message(w)
| intruder_message(triple(w,v,u)) ),
file('SWV015+1.p',unknown),
[] ).
cnf(30,axiom,
( ~ party_of_protocol(u)
| ~ party_of_protocol(v)
| ~ intruder_message(w)
| message(sent(v,u,w)) ),
file('SWV015+1.p',unknown),
[] ).
cnf(27,axiom,
( ~ intruder_message(u)
| ~ intruder_message(v)
| intruder_message(pair(v,u)) ),
file('SWV015+1.p',unknown),
[] ).
cnf(28,axiom,
( ~ party_of_protocol(u)
| ~ intruder_message(v)
| intruder_holds(key(v,u)) ),
file('SWV015+1.p',unknown),
[] ).
cnf(23,axiom,
( ~ intruder_message(quadruple(u,v,w,x))
| intruder_message(u) ),
file('SWV015+1.p',unknown),
[] ).
cnf(24,axiom,
( ~ intruder_message(quadruple(u,v,w,x))
| intruder_message(v) ),
file('SWV015+1.p',unknown),
[] ).
cnf(25,axiom,
( ~ intruder_message(quadruple(u,v,w,x))
| intruder_message(w) ),
file('SWV015+1.p',unknown),
[] ).
cnf(26,axiom,
( ~ intruder_message(quadruple(u,v,w,x))
| intruder_message(x) ),
file('SWV015+1.p',unknown),
[] ).
cnf(20,axiom,
( ~ intruder_message(triple(u,v,w))
| intruder_message(u) ),
file('SWV015+1.p',unknown),
[] ).
cnf(21,axiom,
( ~ intruder_message(triple(u,v,w))
| intruder_message(v) ),
file('SWV015+1.p',unknown),
[] ).
cnf(79,plain,
intruder_message(an_a_nonce),
inference(res,[status(thm),theory(equality)],[77,18]),
[iquote('0:Res:77.0,18.0')] ).
cnf(78,plain,
intruder_message(a),
inference(res,[status(thm),theory(equality)],[77,17]),
[iquote('0:Res:77.0,17.0')] ).
cnf(77,plain,
intruder_message(pair(a,an_a_nonce)),
inference(res,[status(thm),theory(equality)],[16,19]),
[iquote('0:Res:16.0,19.0')] ).
cnf(22,axiom,
( ~ intruder_message(triple(u,v,w))
| intruder_message(w) ),
file('SWV015+1.p',unknown),
[] ).
cnf(19,axiom,
( ~ message(sent(u,v,w))
| intruder_message(w) ),
file('SWV015+1.p',unknown),
[] ).
cnf(17,axiom,
( ~ intruder_message(pair(u,v))
| intruder_message(u) ),
file('SWV015+1.p',unknown),
[] ).
cnf(18,axiom,
( ~ intruder_message(pair(u,v))
| intruder_message(v) ),
file('SWV015+1.p',unknown),
[] ).
cnf(16,axiom,
message(sent(a,b,pair(a,an_a_nonce))),
file('SWV015+1.p',unknown),
[] ).
cnf(15,axiom,
( ~ a_nonce(u)
| ~ a_key(u) ),
file('SWV015+1.p',unknown),
[] ).
cnf(14,axiom,
~ a_nonce(generate_key(u)),
file('SWV015+1.p',unknown),
[] ).
cnf(12,axiom,
t_holds(key(at,a)),
file('SWV015+1.p',unknown),
[] ).
cnf(13,axiom,
t_holds(key(bt,b)),
file('SWV015+1.p',unknown),
[] ).
cnf(10,axiom,
a_stored(pair(b,an_a_nonce)),
file('SWV015+1.p',unknown),
[] ).
cnf(9,axiom,
a_holds(key(at,t)),
file('SWV015+1.p',unknown),
[] ).
cnf(11,axiom,
b_holds(key(bt,t)),
file('SWV015+1.p',unknown),
[] ).
cnf(6,axiom,
a_nonce(generate_expiration_time(u)),
file('SWV015+1.p',unknown),
[] ).
cnf(7,axiom,
a_nonce(generate_b_nonce(u)),
file('SWV015+1.p',unknown),
[] ).
cnf(8,axiom,
a_key(generate_key(u)),
file('SWV015+1.p',unknown),
[] ).
cnf(1,axiom,
party_of_protocol(a),
file('SWV015+1.p',unknown),
[] ).
cnf(2,axiom,
party_of_protocol(b),
file('SWV015+1.p',unknown),
[] ).
cnf(4,axiom,
party_of_protocol(t),
file('SWV015+1.p',unknown),
[] ).
cnf(5,axiom,
a_nonce(an_a_nonce),
file('SWV015+1.p',unknown),
[] ).
cnf(3,axiom,
fresh_to_b(an_a_nonce),
file('SWV015+1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWV015+1 : TPTP v8.1.0. Released v2.4.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n012.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Wed Jun 15 22:27:39 EDT 2022
% 0.12/0.34 % CPUTime :
% 1.08/1.24
% 1.08/1.24 SPASS V 3.9
% 1.08/1.24 SPASS beiseite: Completion found.
% 1.08/1.24 % SZS status CounterSatisfiable
% 1.08/1.24 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.08/1.24 SPASS derived 878 clauses, backtracked 0 clauses, performed 0 splits and kept 445 clauses.
% 1.08/1.24 SPASS allocated 101038 KBytes.
% 1.08/1.24 SPASS spent 0:00:00.90 on the problem.
% 1.08/1.24 0:00:00.04 for the input.
% 1.08/1.24 0:00:00.04 for the FLOTTER CNF translation.
% 1.08/1.24 0:00:00.08 for inferences.
% 1.08/1.24 0:00:00.00 for the backtracking.
% 1.08/1.24 0:00:00.71 for the reduction.
% 1.08/1.24
% 1.08/1.24
% 1.08/1.24 The saturated set of worked-off clauses is :
% 1.08/1.24 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------